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 4926 dmfco 5457 omp1eomlem 6947 ltanqg 7176 genpassl 7300 genpassu 7301 ltexprlemloc 7383 caucvgprlemcanl 7420 cauappcvgprlemladdrl 7433 caucvgprlemladdrl 7454 caucvgprprlemaddq 7484 apneg 8340 lemuldiv 8603 msq11 8624 negiso 8677 avglt2 8917 xleaddadd 9625 iooshf 9690 qtri3or 9975 sq11ap 10413 hashen 10485 fihashdom 10504 cjap 10633 sqrt11ap 10765 xrnegiso 10986 clim2c 11008 climabs0 11031 absefib 11391 efieq1re 11392 nndivides 11412 oddnn02np1 11489 oddge22np1 11490 evennn02n 11491 evennn2n 11492 halfleoddlt 11503 cnntr 12305 cndis 12321 cnpdis 12322 lmres 12328 txhmeo 12399 blininf 12504 cncfmet 12659 |
Copyright terms: Public domain | W3C validator |