| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 3bitr2d | Unicode version | ||
| Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
| Ref | Expression |
|---|---|
| 3bitr2d.1 |
|
| 3bitr2d.2 |
|
| 3bitr2d.3 |
|
| Ref | Expression |
|---|---|
| 3bitr2d |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3bitr2d.1 |
. . 3
| |
| 2 | 3bitr2d.2 |
. . 3
| |
| 3 | 1, 2 | bitr4d 191 |
. 2
|
| 4 | 3bitr2d.3 |
. 2
| |
| 5 | 3, 4 | bitrd 188 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 |
| This theorem is referenced by: ceqsralt 2798 frecsuclem 6491 indpi 7454 cauappcvgprlemladdru 7768 prsrlt 7899 lesub2 8529 ltsub2 8531 rec11ap 8782 avglt1 9275 rpnegap 9807 modqmuladdnn0 10511 expap0 10712 2shfti 11113 mulreap 11146 minmax 11512 lemininf 11516 xrminmax 11547 xrlemininf 11553 modremain 12211 nnwosdc 12331 nn0seqcvgd 12334 divgcdcoprm0 12394 ismgmid 13180 grpsubeq0 13389 grpsubadd 13391 eqg0el 13536 isunitd 13839 lsslss 14114 isridlrng 14215 zndvds 14382 znleval 14386 isxmet2d 14791 xblss2 14848 neibl 14934 ellimc3apf 15103 logbgt0b 15409 lgsne0 15486 lgsabs1 15487 lgsquadlem1 15525 m1lgs 15533 iswomninnlem 15950 |
| Copyright terms: Public domain | W3C validator |