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  830  rspcime  2875  abvor0dc  3475  exmidsssn  4236  euotd  4288  nn0eln0  4657  elabrex  5807  elabrexg  5808  riota5f  5905  nntri3  6564  fin0  6955  omp1eomlem  7169  ctssdccl  7186  ismkvnex  7230  finacn  7289  acnccim  7357  nn1m1nn  9027  xrlttri3  9891  nltpnft  9908  ngtmnft  9911  xrrebnd  9913  xltadd1  9970  xsubge0  9975  xposdif  9976  xlesubadd  9977  xleaddadd  9981  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  fzaddel  10153  elfzomelpfzo  10326  xqltnle  10376  nnesq  10770  hashnncl  10906  zfz1isolemiso  10950  mod2eq1n2dvds  12063  m1exp1  12085  dfgcd3  12204  dvdssq  12225  pcdvdsb  12516  pceq0  12518  issubg3  13400  lmss  14590  lmres  14592  2omap  15750