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 262 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒))) | |
4 | 1, 2, 3 | sylc 65 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: 2falsed 377 biort 933 vtocl2d 3496 vtocl2 3500 vtocl3 3501 rspcime 3564 sbc2or 3725 ralidmOLD 4446 disjprgw 5069 disjprg 5070 euotd 5427 posn 5672 frsn 5674 cnvpo 6190 elabrex 7116 riota5f 7261 smoord 8196 brwdom2 9332 finacn 9806 acacni 9896 dfac13 9898 fin1a2lem10 10165 gch2 10431 gchac 10437 recmulnq 10720 nn1m1nn 11994 nn0sub 12283 xnn0n0n1ge2b 12867 qextltlem 12936 xnn0lem1lt 12978 xsubge0 12995 xlesubadd 12997 iccshftr 13218 iccshftl 13220 iccdil 13222 icccntr 13224 fzaddel 13290 elfzomelpfzo 13491 sqlecan 13925 nnesq 13942 hashdom 14094 swrdspsleq 14378 repswsymballbi 14493 m1exp1 16085 bitsmod 16143 dvdssq 16272 pcdvdsb 16570 vdwmc2 16680 acsfn 17368 subsubc 17568 funcres2b 17612 isipodrs 18255 issubg3 18773 sdrgacs 20069 opnnei 22271 lmss 22449 lmres 22451 cmpfi 22559 xkopt 22806 acufl 23068 lmhmclm 24250 equivcmet 24481 degltlem1 25237 mdegle0 25242 cxple2 25852 rlimcnp3 26117 dchrelbas3 26386 tgcolg 26915 hlbtwn 26972 eupth2lem3lem6 28597 isoun 31034 smatrcl 31746 msrrcl 33505 fz0n 33696 onint1 34638 bj-animbi 34739 bj-nfcsym 35084 matunitlindf 35775 ftc1anclem6 35855 lcvexchlem1 37048 ltrnatb 38151 cdlemg27b 38710 lmhmlvec 40261 fsuppind 40279 dvdsexpnn0 40341 gicabl 40924 dfacbasgrp 40933 rp-fakeimass 41119 or3or 41631 radcnvrat 41932 elabrexg 42589 eliooshift 43044 ellimcabssub0 43158 |
Copyright terms: Public domain | W3C validator |