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  834  rspcime  2914  abvor0dc  3515  exmidsssn  4286  euotd  4341  nn0eln0  4712  elabrex  5887  elabrexg  5888  riota5f  5987  nntri3  6651  fin0  7055  omp1eomlem  7272  ctssdccl  7289  ismkvnex  7333  finacn  7397  acnccim  7469  nn1m1nn  9139  xrlttri3  10005  nltpnft  10022  ngtmnft  10025  xrrebnd  10027  xltadd1  10084  xsubge0  10089  xposdif  10090  xlesubadd  10091  xleaddadd  10095  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzaddel  10267  elfzomelpfzo  10449  xqltnle  10499  nnesq  10893  hashnncl  11029  zfz1isolemiso  11074  swrdspsleq  11214  mod2eq1n2dvds  12405  m1exp1  12427  dfgcd3  12546  dvdssq  12567  pcdvdsb  12858  pceq0  12860  issubg3  13744  lmss  14935  lmres  14937  2omap  16418