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  2915  abvor0dc  3516  exmidsssn  4290  euotd  4345  nn0eln0  4716  elabrex  5893  elabrexg  5894  riota5f  5993  nntri3  6660  modom  6989  fin0  7067  omp1eomlem  7284  ctssdccl  7301  ismkvnex  7345  finacn  7409  acnccim  7481  nn1m1nn  9151  xrlttri3  10022  nltpnft  10039  ngtmnft  10042  xrrebnd  10044  xltadd1  10101  xsubge0  10106  xposdif  10107  xlesubadd  10108  xleaddadd  10112  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  fzaddel  10284  elfzomelpfzo  10466  xqltnle  10517  nnesq  10911  hashnncl  11047  zfz1isolemiso  11093  swrdspsleq  11238  mod2eq1n2dvds  12430  m1exp1  12452  dfgcd3  12571  dvdssq  12592  pcdvdsb  12883  pceq0  12885  issubg3  13769  lmss  14960  lmres  14962  2omap  16530