Theorem 2thd 174

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rspcime  2796  abvor0dc  3386  exmidsssn  4125  euotd  4176  nn0eln0  4533  elabrex  5659  riota5f  5754  nntri3  6393  fin0  6779  omp1eomlem  6979  ctssdccl  6996  ismkvnex  7029  nn1m1nn  8738  xrlttri3  9583  nltpnft  9597  ngtmnft  9600  xrrebnd  9602  xltadd1  9659  xsubge0  9664  xposdif  9665  xlesubadd  9666  xleaddadd  9670  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  fzaddel  9839  elfzomelpfzo  10008  nnesq  10411  hashnncl  10542  zfz1isolemiso  10582  mod2eq1n2dvds  11576  m1exp1  11598  dfgcd3  11698  dvdssq  11719  lmss  12415  lmres  12417