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:  biort  819  rspcime  2836  abvor0dc  3431  exmidsssn  4180  euotd  4231  nn0eln0  4596  elabrex  5725  riota5f  5821  nntri3  6461  fin0  6847  omp1eomlem  7055  ctssdccl  7072  ismkvnex  7115  nn1m1nn  8871  xrlttri3  9729  nltpnft  9746  ngtmnft  9749  xrrebnd  9751  xltadd1  9808  xsubge0  9813  xposdif  9814  xlesubadd  9815  xleaddadd  9819  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  fzaddel  9990  elfzomelpfzo  10162  nnesq  10570  hashnncl  10705  zfz1isolemiso  10748  mod2eq1n2dvds  11812  m1exp1  11834  dfgcd3  11939  dvdssq  11960  pcdvdsb  12247  pceq0  12249  lmss  12846  lmres  12848