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  815  rspcime  2823  abvor0dc  3417  exmidsssn  4163  euotd  4214  nn0eln0  4579  elabrex  5708  riota5f  5804  nntri3  6444  fin0  6830  omp1eomlem  7038  ctssdccl  7055  ismkvnex  7098  nn1m1nn  8851  xrlttri3  9704  nltpnft  9718  ngtmnft  9721  xrrebnd  9723  xltadd1  9780  xsubge0  9785  xposdif  9786  xlesubadd  9787  xleaddadd  9791  iccshftr  9898  iccshftl  9900  iccdil  9902  icccntr  9904  fzaddel  9961  elfzomelpfzo  10130  nnesq  10537  hashnncl  10670  zfz1isolemiso  10710  mod2eq1n2dvds  11769  m1exp1  11791  dfgcd3  11893  dvdssq  11914  lmss  12646  lmres  12648