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

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
StepHypRef Expression
1 2thd.1 . 2 (𝜑𝜓)
2 2thd.2 . 2 (𝜑𝜒)
3 pm5.1im 173 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 62 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
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  829  rspcime  2848  abvor0dc  3446  exmidsssn  4202  euotd  4254  nn0eln0  4619  elabrex  5758  riota5f  5854  nntri3  6497  fin0  6884  omp1eomlem  7092  ctssdccl  7109  ismkvnex  7152  nn1m1nn  8935  xrlttri3  9795  nltpnft  9812  ngtmnft  9815  xrrebnd  9817  xltadd1  9874  xsubge0  9879  xposdif  9880  xlesubadd  9881  xleaddadd  9885  iccshftr  9992  iccshftl  9994  iccdil  9996  icccntr  9998  fzaddel  10056  elfzomelpfzo  10228  nnesq  10636  hashnncl  10770  zfz1isolemiso  10814  mod2eq1n2dvds  11878  m1exp1  11900  dfgcd3  12005  dvdssq  12026  pcdvdsb  12313  pceq0  12315  issubg3  13005  lmss  13639  lmres  13641
  Copyright terms: Public domain W3C validator