let
A
be
QC-alphabet
;
:: thesis:
for
p
,
q
being
Element
of
CQC-WFF
A
holds
(
p
<=>
q
)
=>
(
p
=>
q
)
in
TAUT
A
let
p
,
q
be
Element
of
CQC-WFF
A
;
:: thesis:
(
p
<=>
q
)
=>
(
p
=>
q
)
in
TAUT
A
p
<=>
q
=
(
p
=>
q
)
'&'
(
q
=>
p
)
by
QC_LANG2:def 4
;
hence
(
p
<=>
q
)
=>
(
p
=>
q
)
in
TAUT
A
by
Th19
;
:: thesis:
verum