Theorem 2thd 173

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 171	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 61	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  abvor0dc  3306  euotd  4081  nn0eln0  4433  elabrex  5537  riota5f  5632  nntri3  6258  fin0  6601  nn1m1nn  8440  xrlttri3  9267  nltpnft  9279  ngtmnft  9280  xrrebnd  9281  iccshftr  9411  iccshftl  9413  iccdil  9415  icccntr  9417  fzaddel  9473  elfzomelpfzo  9642  nnesq  10073  hashnncl  10204  zfz1isolemiso  10244  mod2eq1n2dvds  11157  m1exp1  11179  dfgcd3  11277  dvdssq  11298