Theorem 2thd 268

Description: Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012.)

Hypotheses

Ref	Expression
2thd.1	⊢ (𝜑 → 𝜓)
2thd.2	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
2thd	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem 2thd

Step	Hyp	Ref	Expression
1		2thd.1	. 2 ⊢ (𝜑 → 𝜓)
2		2thd.2	. 2 ⊢ (𝜑 → 𝜒)
3		pm5.1im 266	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 66	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  2falsed  379  biort  949  vtocl2d  3524  rspcime  3582  sbc2or  3748  nrmod  3839  disjprg  5099  euotd  5486  posn  5737  frsn  5739  cnvpo  6289  elabrex  7244  elabrexg  7245  riota5f  7403  smoord  8366  brwdom2  9560  finacn  10122  acacni  10212  dfac13  10214  fin1a2lem10  10480  gch2  10753  gchac  10759  recmulnq  11042  nn1m1nn  12349  nn0sub  12649  xnn0n0n1ge2b  13254  qextltlem  13325  xnn0lem1lt  13367  xsubge0  13384  xlesubadd  13386  iccshftr  13610  iccshftl  13612  iccdil  13614  icccntr  13616  fzaddel  13685  elfzomelpfzo  13900  sqlecan  14346  nnesq  14364  hashdom  14516  swrdspsleq  14808  repswsymballbi  14924  m1exp1  16539  bitsmod  16599  dvdssq  16735  pcdvdsb  17040  vdwmc2  17150  acsfn  17826  subsubc  18021  funcres2b  18065  isipodrs  18704  issubg3  19348  sdrgacs  21051  lmhmlvec  21378  matunitlindf  22989  opnnei  23431  lmss  23609  lmres  23611  cmpfi  23719  xkopt  23967  acufl  24229  lmhmclm  25401  equivcmet  25631  degltlem1  26383  mdegle0  26388  cxple2  27018  rlimcnp3  27288  dchrelbas3  27558  tgcolg  29010  hlbtwn  29070  eupth2lem3lem6  30827  ifnebib  33138  isoun  33288  subsdrg  33853  unitprodclb  33937  smatrcl  34421  msrrcl  36287  fz0n  36475  onint1  37217  bj-animbi  37408  bj-nfcsym  37791  ftc1anclem6  38596  lcvexchlem1  40071  ltrnatb  41174  cdlemg27b  41733  dvdsexpnn0  43366  fsuppind  43598  gicabl  44085  dfacbasgrp  44094  rp-fakeimass  44497  or3or  45008  radcnvrat  45283  eliooshift  46487  ellimcabssub0  46598  resccat  50151