![]() |
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 255 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒))) | |
4 | 1, 2, 3 | sylc 65 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ 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: sbc2or 3642 ralidm 4268 disjprg 4839 euotd 5169 posn 5392 frsn 5394 cnvpo 5892 elabrex 6729 riota5f 6864 smoord 7701 brwdom2 8720 finacn 9159 acacni 9250 dfac13 9252 fin1a2lem10 9519 gch2 9785 gchac 9791 recmulnq 10074 nn1m1nn 11334 nn0sub 11632 xnn0n0n1ge2b 12212 qextltlem 12282 xsubge0 12340 xlesubadd 12342 iccshftr 12560 iccshftl 12562 iccdil 12564 icccntr 12566 fzaddel 12629 elfzomelpfzo 12827 sqlecan 13225 nnesq 13242 hashdom 13418 swrdspsleq 13703 repswsymballbi 13860 znnenlemOLD 15276 m1exp1 15429 bitsmod 15493 dvdssq 15615 pcdvdsb 15906 vdwmc2 16016 acsfn 16634 subsubc 16827 funcres2b 16871 isipodrs 17476 issubg3 17925 opnnei 21253 lmss 21431 lmres 21433 cmpfi 21540 xkopt 21787 acufl 22049 lmhmclm 23214 equivcmet 23443 degltlem1 24173 mdegle0 24178 cxple2 24784 rlimcnp3 25046 dchrelbas3 25315 tgcolg 25805 hlbtwn 25862 eupth2lem3lem6 27578 isoun 29997 smatrcl 30378 msrrcl 31957 fz0n 32130 onint1 32956 bj-nfcsym 33377 matunitlindf 33896 ftc1anclem6 33978 lcvexchlem1 35055 ltrnatb 36158 cdlemg27b 36717 gicabl 38454 dfacbasgrp 38463 sdrgacs 38556 rp-fakeimass 38641 or3or 39101 radcnvrat 39295 elabrexg 39966 eliooshift 40477 ellimcabssub0 40593 |
Copyright terms: Public domain | W3C validator |