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  4339  euotd  4395  nn0eln0  4767  elabrex  5963  elabrexg  5964  riota5f  6065  nntri3  6770  modom  7108  fin0  7189  2omap  7318  omp1eomlem  7434  ctssdccl  7451  ismkvnex  7495  finacn  7560  acnccim  7638  nn1m1nn  9322  xrlttri3  10199  nltpnft  10216  ngtmnft  10219  xrrebnd  10221  xltadd1  10278  xsubge0  10283  xposdif  10284  xlesubadd  10285  xleaddadd  10289  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  fzaddel  10465  elfzomelpfzo  10649  xqltnle  10702  nnesq  11097  hashnncl  11234  zfz1isolemiso  11291  swrdspsleq  11439  mod2eq1n2dvds  12646  m1exp1  12668  dfgcd3  12787  dvdssq  12808  pcdvdsb  13099  pceq0  13101  issubg3  13995  lmss  15347  lmres  15349  eupth2lem3lem6fi  16712