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  2849  abvor0dc  3447  exmidsssn  4203  euotd  4255  nn0eln0  4620  elabrex  5759  riota5f  5855  nntri3  6498  fin0  6885  omp1eomlem  7093  ctssdccl  7110  ismkvnex  7153  nn1m1nn  8937  xrlttri3  9797  nltpnft  9814  ngtmnft  9817  xrrebnd  9819  xltadd1  9876  xsubge0  9881  xposdif  9882  xlesubadd  9883  xleaddadd  9887  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  fzaddel  10059  elfzomelpfzo  10231  nnesq  10640  hashnncl  10775  zfz1isolemiso  10819  mod2eq1n2dvds  11884  m1exp1  11906  dfgcd3  12011  dvdssq  12032  pcdvdsb  12319  pceq0  12321  issubg3  13052  lmss  13749  lmres  13751