Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ w3a 1086 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-3an 1088 |
This theorem is referenced by: dalemrot
37925 dath2
38005 cdleme18d
38563 cdleme20i
38585 cdleme20j
38586 cdleme20l2
38589 cdleme20l
38590 cdleme20m
38591 cdleme20
38592 cdleme21j
38604 cdleme22eALTN
38613 cdleme26eALTN
38629 cdlemk16a
39124 cdlemk12u-2N
39158 cdlemk21-2N
39159 cdlemk22
39161 cdlemk31
39164 cdlemk11ta
39197 |