ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2thd GIF version

Theorem 2thd 174
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
StepHypRef Expression
1 2thd.1 . 2 (𝜑𝜓)
2 2thd.2 . 2 (𝜑𝜒)
3 pm5.1im 172 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 62 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  rspcime  2770  abvor0dc  3356  exmidsssn  4095  euotd  4146  nn0eln0  4503  elabrex  5627  riota5f  5722  nntri3  6361  fin0  6747  omp1eomlem  6947  ctssdccl  6964  ismkvnex  6997  nn1m1nn  8702  xrlttri3  9538  nltpnft  9552  ngtmnft  9555  xrrebnd  9557  xltadd1  9614  xsubge0  9619  xposdif  9620  xlesubadd  9621  xleaddadd  9625  iccshftr  9732  iccshftl  9734  iccdil  9736  icccntr  9738  fzaddel  9794  elfzomelpfzo  9963  nnesq  10366  hashnncl  10497  zfz1isolemiso  10537  mod2eq1n2dvds  11488  m1exp1  11510  dfgcd3  11610  dvdssq  11631  lmss  12326  lmres  12328
  Copyright terms: Public domain W3C validator