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  829  rspcime  2848  abvor0dc  3446  exmidsssn  4202  euotd  4254  nn0eln0  4619  elabrex  5758  riota5f  5854  nntri3  6497  fin0  6884  omp1eomlem  7092  ctssdccl  7109  ismkvnex  7152  nn1m1nn  8935  xrlttri3  9795  nltpnft  9812  ngtmnft  9815  xrrebnd  9817  xltadd1  9874  xsubge0  9879  xposdif  9880  xlesubadd  9881  xleaddadd  9885  iccshftr  9992  iccshftl  9994  iccdil  9996  icccntr  9998  fzaddel  10056  elfzomelpfzo  10228  nnesq  10636  hashnncl  10770  zfz1isolemiso  10814  mod2eq1n2dvds  11878  m1exp1  11900  dfgcd3  12005  dvdssq  12026  pcdvdsb  12313  pceq0  12315  issubg3  13005  lmss  13639  lmres  13641