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  831  rspcime  2888  abvor0dc  3488  exmidsssn  4254  euotd  4307  nn0eln0  4676  elabrex  5839  elabrexg  5840  riota5f  5937  nntri3  6596  fin0  6997  omp1eomlem  7211  ctssdccl  7228  ismkvnex  7272  finacn  7332  acnccim  7404  nn1m1nn  9074  xrlttri3  9939  nltpnft  9956  ngtmnft  9959  xrrebnd  9961  xltadd1  10018  xsubge0  10023  xposdif  10024  xlesubadd  10025  xleaddadd  10029  iccshftr  10136  iccshftl  10138  iccdil  10140  icccntr  10142  fzaddel  10201  elfzomelpfzo  10382  xqltnle  10432  nnesq  10826  hashnncl  10962  zfz1isolemiso  11006  swrdspsleq  11143  mod2eq1n2dvds  12265  m1exp1  12287  dfgcd3  12406  dvdssq  12427  pcdvdsb  12718  pceq0  12720  issubg3  13603  lmss  14793  lmres  14795  2omap  16071