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  4285  euotd  4340  nn0eln0  4711  elabrex  5880  elabrexg  5881  riota5f  5980  nntri3  6641  fin0  7043  omp1eomlem  7257  ctssdccl  7274  ismkvnex  7318  finacn  7382  acnccim  7454  nn1m1nn  9124  xrlttri3  9989  nltpnft  10006  ngtmnft  10009  xrrebnd  10011  xltadd1  10068  xsubge0  10073  xposdif  10074  xlesubadd  10075  xleaddadd  10079  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  fzaddel  10251  elfzomelpfzo  10432  xqltnle  10482  nnesq  10876  hashnncl  11012  zfz1isolemiso  11056  swrdspsleq  11194  mod2eq1n2dvds  12385  m1exp1  12407  dfgcd3  12526  dvdssq  12547  pcdvdsb  12838  pceq0  12840  issubg3  13724  lmss  14914  lmres  14916  2omap  16318