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  7287  acnccim  7355  nn1m1nn  9025  xrlttri3  9889  nltpnft  9906  ngtmnft  9909  xrrebnd  9911  xltadd1  9968  xsubge0  9973  xposdif  9974  xlesubadd  9975  xleaddadd  9979  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  fzaddel  10151  elfzomelpfzo  10324  xqltnle  10374  nnesq  10768  hashnncl  10904  zfz1isolemiso  10948  mod2eq1n2dvds  12061  m1exp1  12083  dfgcd3  12202  dvdssq  12223  pcdvdsb  12514  pceq0  12516  issubg3  13398  lmss  14566  lmres  14568  2omap  15726