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

Theorem 2thd 164
 Description: Two truths are equivalent (deduction rule). (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 162 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 56 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  abvor0dc  3242  euotd  3991  nn0eln0  4341  elabrex  5397  riota5f  5492  nntri3  6075  fin0  6342  nn1m1nn  7932  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  xrrebnd  8732  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  fzaddel  8922  elfzomelpfzo  9087  nnesq  9368
 Copyright terms: Public domain W3C validator