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  5897  elabrexg  5898  riota5f  5997  nntri3  6664  modom  6993  fin0  7073  omp1eomlem  7292  ctssdccl  7309  ismkvnex  7353  finacn  7418  acnccim  7490  nn1m1nn  9160  xrlttri3  10031  nltpnft  10048  ngtmnft  10051  xrrebnd  10053  xltadd1  10110  xsubge0  10115  xposdif  10116  xlesubadd  10117  xleaddadd  10121  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  fzaddel  10293  elfzomelpfzo  10475  xqltnle  10526  nnesq  10920  hashnncl  11056  zfz1isolemiso  11102  swrdspsleq  11247  mod2eq1n2dvds  12439  m1exp1  12461  dfgcd3  12580  dvdssq  12601  pcdvdsb  12892  pceq0  12894  issubg3  13778  lmss  14969  lmres  14971  2omap  16594