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  2791  abvor0dc  3381  exmidsssn  4120  euotd  4171  nn0eln0  4528  elabrex  5652  riota5f  5747  nntri3  6386  fin0  6772  omp1eomlem  6972  ctssdccl  6989  ismkvnex  7022  nn1m1nn  8731  xrlttri3  9576  nltpnft  9590  ngtmnft  9593  xrrebnd  9595  xltadd1  9652  xsubge0  9657  xposdif  9658  xlesubadd  9659  xleaddadd  9663  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  fzaddel  9832  elfzomelpfzo  10001  nnesq  10404  hashnncl  10535  zfz1isolemiso  10575  mod2eq1n2dvds  11565  m1exp1  11587  dfgcd3  11687  dvdssq  11708  lmss  12404  lmres  12406