Theorem 2thd 175

Description: Two truths are equivalent (deduction form). (Contributed by NM, 3-Jun-2012.) (Revised by NM, 29-Jan-2013.)

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 173	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 62	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biort  837  rspcime  2918  abvor0dc  3520  exmidsssn  4298  euotd  4353  nn0eln0  4724  elabrex  5908  elabrexg  5909  riota5f  6008  nntri3  6708  modom  7037  fin0  7117  omp1eomlem  7336  ctssdccl  7353  ismkvnex  7397  finacn  7462  acnccim  7534  nn1m1nn  9203  xrlttri3  10076  nltpnft  10093  ngtmnft  10096  xrrebnd  10098  xltadd1  10155  xsubge0  10160  xposdif  10161  xlesubadd  10162  xleaddadd  10166  iccshftr  10273  iccshftl  10275  iccdil  10277  icccntr  10279  fzaddel  10339  elfzomelpfzo  10522  xqltnle  10573  nnesq  10967  hashnncl  11103  zfz1isolemiso  11149  swrdspsleq  11297  mod2eq1n2dvds  12503  m1exp1  12525  dfgcd3  12644  dvdssq  12665  pcdvdsb  12956  pceq0  12958  issubg3  13842  lmss  15040  lmres  15042  eupth2lem3lem6fi  16395  2omap  16698