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 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biort  841  rspcime  2937  abvor0dc  3545  exmidsssn  4341  euotd  4397  nn0eln0  4769  elabrex  5966  elabrexg  5967  riota5f  6068  nntri3  6774  modom  7112  fin0  7193  2omap  7324  omp1eomlem  7440  ctssdccl  7457  ismkvnex  7501  finacn  7566  acnccim  7644  nn1m1nn  9331  xrlttri3  10216  nltpnft  10233  ngtmnft  10236  xrrebnd  10238  xltadd1  10295  xsubge0  10300  xposdif  10301  xlesubadd  10302  xleaddadd  10306  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  fzaddel  10482  elfzomelpfzo  10666  xqltnle  10719  flaplt  10739  nnesq  11118  nn0sqdc  11168  hashnncl  11256  zfz1isolemiso  11313  swrdspsleq  11461  mod2eq1n2dvds  12671  m1exp1  12693  dfgcd3  12812  dvdssq  12833  pcdvdsb  13128  pceq0  13130  issubg3  14054  lmss  15472  lmres  15474  eupth2lem3lem6fi  16917