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

Theorem 2thd 173
 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 171 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 61 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  abvor0dc  3276  euotd  4017  nn0eln0  4367  elabrex  5429  riota5f  5523  nntri3  6141  fin0  6419  nn1m1nn  8124  xrlttri3  8948  nltpnft  8960  ngtmnft  8961  xrrebnd  8962  iccshftr  9092  iccshftl  9094  iccdil  9096  icccntr  9098  fzaddel  9153  elfzomelpfzo  9317  nnesq  9689  sizenncl  9820  mod2eq1n2dvds  10423  m1exp1  10445  dfgcd3  10543  dvdssq  10564
 Copyright terms: Public domain W3C validator