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

Theorem adantrd 264
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 102 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 28 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem is referenced by:  syldan  266  jaoa  640  prlem1  880  equveli  1642  elssabg  3902  suctr  4158  fvun1  5239  opabbrex  5549  poxp  5853  tposfo2  5882  1idprl  6688  1idpru  6689  uzind  8349  xrlttr  8716  fzen  8907  fz0fzelfz0  8984  bj-om  10061
  Copyright terms: Public domain W3C validator