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  837  rspcime  2931  abvor0dc  3536  exmidsssn  4320  euotd  4376  nn0eln0  4747  elabrex  5936  elabrexg  5937  riota5f  6038  nntri3  6743  modom  7074  fin0  7155  2omap  7282  omp1eomlem  7398  ctssdccl  7415  ismkvnex  7459  finacn  7524  acnccim  7602  nn1m1nn  9272  xrlttri3  10149  nltpnft  10166  ngtmnft  10169  xrrebnd  10171  xltadd1  10228  xsubge0  10233  xposdif  10234  xlesubadd  10235  xleaddadd  10239  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  fzaddel  10414  elfzomelpfzo  10598  xqltnle  10651  nnesq  11046  hashnncl  11183  zfz1isolemiso  11236  swrdspsleq  11384  mod2eq1n2dvds  12590  m1exp1  12612  dfgcd3  12731  dvdssq  12752  pcdvdsb  13043  pceq0  13045  issubg3  13945  lmss  15237  lmres  15239  eupth2lem3lem6fi  16592