theorem :: QC_LANG2:35

for A being QC-alphabet
for H being Element of QC-WFF A st H is biconditional holds
( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) by Th4;