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  836  rspcime  2917  abvor0dc  3518  exmidsssn  4292  euotd  4347  nn0eln0  4718  elabrex  5898  elabrexg  5899  riota5f  5998  nntri3  6665  modom  6994  fin0  7074  omp1eomlem  7293  ctssdccl  7310  ismkvnex  7354  finacn  7419  acnccim  7491  nn1m1nn  9161  xrlttri3  10032  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xltadd1  10111  xsubge0  10116  xposdif  10117  xlesubadd  10118  xleaddadd  10122  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzaddel  10294  elfzomelpfzo  10477  xqltnle  10528  nnesq  10922  hashnncl  11058  zfz1isolemiso  11104  swrdspsleq  11252  mod2eq1n2dvds  12445  m1exp1  12467  dfgcd3  12586  dvdssq  12607  pcdvdsb  12898  pceq0  12900  issubg3  13784  lmss  14976  lmres  14978  eupth2lem3lem6fi  16328  2omap  16620