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:  biort  824  rspcime  2841  abvor0dc  3438  exmidsssn  4188  euotd  4239  nn0eln0  4604  elabrex  5737  riota5f  5833  nntri3  6476  fin0  6863  omp1eomlem  7071  ctssdccl  7088  ismkvnex  7131  nn1m1nn  8896  xrlttri3  9754  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xltadd1  9833  xsubge0  9838  xposdif  9839  xlesubadd  9840  xleaddadd  9844  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fzaddel  10015  elfzomelpfzo  10187  nnesq  10595  hashnncl  10730  zfz1isolemiso  10774  mod2eq1n2dvds  11838  m1exp1  11860  dfgcd3  11965  dvdssq  11986  pcdvdsb  12273  pceq0  12275  lmss  13040  lmres  13042
  Copyright terms: Public domain W3C validator