Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr4rd | Unicode version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr4d.1 | |
3bitr4d.2 | |
3bitr4d.3 |
Ref | Expression |
---|---|
3bitr4rd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4d.3 | . . 3 | |
2 | 3bitr4d.1 | . . 3 | |
3 | 1, 2 | bitr4d 190 | . 2 |
4 | 3bitr4d.2 | . 2 | |
5 | 3, 4 | bitr4d 190 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: inimasn 5018 dmfco 5551 omp1eomlem 7053 ltanqg 7335 genpassl 7459 genpassu 7460 ltexprlemloc 7542 caucvgprlemcanl 7579 cauappcvgprlemladdrl 7592 caucvgprlemladdrl 7613 caucvgprprlemaddq 7643 apneg 8503 lemuldiv 8770 msq11 8791 negiso 8844 avglt2 9090 xleaddadd 9817 iooshf 9882 qtri3or 10172 sq11ap 10616 hashen 10691 fihashdom 10710 cjap 10842 sqrt11ap 10974 mingeb 11177 xrnegiso 11197 clim2c 11219 climabs0 11242 absefib 11705 efieq1re 11706 nndivides 11731 oddnn02np1 11811 oddge22np1 11812 evennn02n 11813 evennn2n 11814 halfleoddlt 11825 pc2dvds 12255 pcmpt 12267 cnntr 12823 cndis 12839 cnpdis 12840 lmres 12846 txhmeo 12917 blininf 13022 cncfmet 13177 |
Copyright terms: Public domain | W3C validator |