| 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 263 | . 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒))) | |
| 4 | 1, 2, 3 | sylc 65 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: 2falsed 376 biort 936 vtocl2d 3562 vtocl2 3566 vtocl3 3567 rspcime 3627 sbc2or 3797 disjprg 5139 euotd 5518 posn 5771 frsn 5773 cnvpo 6307 elabrex 7262 elabrexg 7263 riota5f 7416 smoord 8405 brwdom2 9613 finacn 10090 acacni 10181 dfac13 10183 fin1a2lem10 10449 gch2 10715 gchac 10721 recmulnq 11004 nn1m1nn 12287 nn0sub 12576 xnn0n0n1ge2b 13174 qextltlem 13244 xnn0lem1lt 13286 xsubge0 13303 xlesubadd 13305 iccshftr 13526 iccshftl 13528 iccdil 13530 icccntr 13532 fzaddel 13598 elfzomelpfzo 13810 sqlecan 14248 nnesq 14266 hashdom 14418 swrdspsleq 14703 repswsymballbi 14818 m1exp1 16413 bitsmod 16473 dvdssq 16604 pcdvdsb 16907 vdwmc2 17017 acsfn 17702 subsubc 17898 funcres2b 17942 isipodrs 18582 issubg3 19162 sdrgacs 20802 lmhmlvec 21109 opnnei 23128 lmss 23306 lmres 23308 cmpfi 23416 xkopt 23663 acufl 23925 lmhmclm 25120 equivcmet 25351 degltlem1 26111 mdegle0 26116 cxple2 26739 rlimcnp3 27010 dchrelbas3 27282 tgcolg 28562 hlbtwn 28619 eupth2lem3lem6 30252 ifnebib 32562 isoun 32711 unitprodclb 33417 smatrcl 33795 msrrcl 35548 fz0n 35731 onint1 36450 bj-animbi 36560 bj-nfcsym 36900 matunitlindf 37625 ftc1anclem6 37705 lcvexchlem1 39035 ltrnatb 40139 cdlemg27b 40698 dvdsexpnn0 42369 fsuppind 42600 gicabl 43111 dfacbasgrp 43120 rp-fakeimass 43525 or3or 44036 radcnvrat 44333 eliooshift 45519 ellimcabssub0 45632 |
| Copyright terms: Public domain | W3C validator |