Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2thd | Structured version Visualization version GIF version |
Description: Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012.) |
Ref | Expression |
---|---|
2thd.1 | ⊢ (𝜑 → 𝜓) |
2thd.2 | ⊢ (𝜑 → 𝜒) |
Ref | Expression |
---|---|
2thd | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2thd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | 2thd.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | pm5.1im 264 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒))) | |
4 | 1, 2, 3 | sylc 65 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: biort 929 vtocl2d 3558 vtocl2 3562 vtocl3 3564 rspcime 3626 sbc2or 3780 ralidm 4453 disjprgw 5053 disjprg 5054 euotd 5395 posn 5631 frsn 5633 cnvpo 6132 elabrex 6993 riota5f 7131 smoord 7993 brwdom2 9026 finacn 9465 acacni 9555 dfac13 9557 fin1a2lem10 9820 gch2 10086 gchac 10092 recmulnq 10375 nn1m1nn 11647 nn0sub 11936 xnn0n0n1ge2b 12516 qextltlem 12585 xnn0lem1lt 12627 xsubge0 12644 xlesubadd 12646 iccshftr 12862 iccshftl 12864 iccdil 12866 icccntr 12868 fzaddel 12931 elfzomelpfzo 13131 sqlecan 13561 nnesq 13578 hashdom 13730 swrdspsleq 14017 repswsymballbi 14132 m1exp1 15717 bitsmod 15775 dvdssq 15901 pcdvdsb 16195 vdwmc2 16305 acsfn 16920 subsubc 17113 funcres2b 17157 isipodrs 17761 issubg3 18237 sdrgacs 19511 opnnei 21658 lmss 21836 lmres 21838 cmpfi 21946 xkopt 22193 acufl 22455 lmhmclm 23620 equivcmet 23849 degltlem1 24595 mdegle0 24600 cxple2 25207 rlimcnp3 25473 dchrelbas3 25742 tgcolg 26268 hlbtwn 26325 eupth2lem3lem6 27940 isoun 30364 smatrcl 30961 msrrcl 32688 fz0n 32860 onint1 33695 bj-animbi 33792 bj-nfcsym 34113 matunitlindf 34772 ftc1anclem6 34854 lcvexchlem1 36052 ltrnatb 37155 cdlemg27b 37714 lmhmlvec 39028 gicabl 39579 dfacbasgrp 39588 rp-fakeimass 39758 or3or 40251 radcnvrat 40526 elabrexg 41183 eliooshift 41662 ellimcabssub0 41778 |
Copyright terms: Public domain | W3C validator |