![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr4ri | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
Ref | Expression |
---|---|
3bitr4i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr4i.2 | ⊢ (𝜒 ↔ 𝜑) |
3bitr4i.3 | ⊢ (𝜃 ↔ 𝜓) |
Ref | Expression |
---|---|
3bitr4ri | ⊢ (𝜃 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4i.2 | . 2 ⊢ (𝜒 ↔ 𝜑) | |
2 | 3bitr4i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 3bitr4i.3 | . . 3 ⊢ (𝜃 ↔ 𝜓) | |
4 | 2, 3 | bitr4i 270 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | bitr2i 268 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 |
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 199 |
This theorem is referenced by: biadan 807 pm4.78 919 xor 998 cases2 1029 nannanOLD 1472 nic-ax 1637 2sb5 2211 2sb6 2212 dfsb7 2213 2sb5rf 2419 2sb6rf 2420 eu6lem 2590 eu6 2591 moabsOLD 2631 2mo2 2680 2eu7 2691 2eu8 2692 euae 2693 ralanidOLD 3114 r3al 3147 risset 3208 r2exlem 3242 ralxpxfr2d 3549 reuind 3648 undif3 4147 unab 4152 inab 4153 n0el 4202 inssdif0 4210 ssundif 4311 ralf0 4335 raldifsnb 4600 pwtp 4704 unipr 4722 uni0b 4734 iinuni 4883 reusv2lem4 5152 pwtr 5199 opthprc 5463 xpiundir 5470 xpsspw 5529 relun 5531 inopab 5548 difopab 5549 ralxpf 5564 dmiun 5629 elidinxp 5754 inisegn0 5799 rniun 5844 imaco 5941 rnco 5942 mptfnf 6311 fnopabg 6313 dff1o2 6447 brprcneu 6489 idref 6730 imaiun 6828 sorpss 7271 opabex3d 7477 opabex3rd 7478 opabex3 7479 ovmptss 7595 fnsuppres 7659 rankc1 9092 aceq1 9336 dfac10 9356 fin41 9663 axgroth6 10047 genpass 10228 infm3 11400 prime 11875 elixx3g 12566 elfz2 12714 elfzuzb 12717 rpnnen2lem12 15437 divalgb 15614 1nprm 15878 maxprmfct 15908 vdwmc 16169 imasleval 16669 issubm 17828 issubg3 18094 efgrelexlemb 18649 ist1-2 21675 unisngl 21855 elflim2 22292 isfcls 22337 istlm 22512 isnlm 23003 ishl2 23692 ovoliunlem1 23822 erclwwlkref 27551 erclwwlknref 27609 0wlk 27661 h1de2ctlem 29129 nonbooli 29225 5oalem7 29234 ho01i 29402 rnbra 29681 cvnbtwn3 29862 chrelat2i 29939 moel 30050 difrab2 30056 uniinn0 30088 disjex 30126 maprnin 30244 ordtconnlem1 30844 esum2dlem 31028 eulerpartgbij 31308 eulerpartlemr 31310 eulerpartlemn 31317 ballotlem2 31425 bnj976 31730 bnj1185 31746 bnj543 31845 bnj571 31858 bnj611 31870 bnj916 31885 bnj1000 31893 bnj1040 31922 iscvm 32124 untuni 32488 dfso3 32503 dffr5 32542 elima4 32572 brtxpsd3 32911 brbigcup 32913 fixcnv 32923 ellimits 32925 elfuns 32930 brimage 32941 brcart 32947 brimg 32952 brapply 32953 brcup 32954 brcap 32955 dfrdg4 32966 dfint3 32967 ellines 33167 elicc3 33219 bj-snsetex 33826 bj-snglc 33832 bj-projun 33857 bj-vjust 33890 wl-cases2-dnf 34226 poimirlem27 34393 mblfinlem2 34404 iscrngo2 34750 n0elqs 35061 inxpxrn 35121 eqvrelcoss3 35331 prtlem70 35471 prtlem100 35473 prtlem15 35489 prter2 35495 lcvnbtwn3 35642 ishlat1 35966 ishlat2 35967 hlrelat2 36017 islpln5 36149 islvol5 36193 pclclN 36505 cdleme0nex 36904 aaitgo 39192 isdomn3 39234 imaiun1 39393 relexp0eq 39443 ntrk1k3eqk13 39797 2sbc6g 40198 2sbc5g 40199 2reu7 42746 2reu8 42747 alsconv 44288 |
Copyright terms: Public domain | W3C validator |