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

Theorem adantrd 279
Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
Hypothesis
Ref Expression
adantrd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
adantrd (𝜑 → ((𝜓𝜃) → 𝜒))

Proof of Theorem adantrd
StepHypRef Expression
1 simpl 109 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 32 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem is referenced by:  syldan  282  jaoa  721  prlem1  975  equveli  1781  elssabg  4191  suctr  4466  fvun1  5639  opabbrex  5979  poxp  6308  tposfo2  6343  1idprl  7685  1idpru  7686  uzind  9466  xrlttr  9899  fzen  10147  fz0fzelfz0  10231  ccatsymb  11033  fisumss  11622  fprodssdc  11820  zeqzmulgcd  12210  lcmgcdlem  12318  lcmdvds  12320  cncongr2  12345  exprmfct  12379  pceu  12537  infpnlem1  12601  isghm  13497  ringadd2  13707  metrest  14896  bj-charfunbi  15611  bj-om  15737
  Copyright terms: Public domain W3C validator