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  4467  fvun1  5644  opabbrex  5988  poxp  6317  tposfo2  6352  1idprl  7702  1idpru  7703  uzind  9483  xrlttr  9916  fzen  10164  fz0fzelfz0  10248  ccatsymb  11056  fisumss  11645  fprodssdc  11843  zeqzmulgcd  12233  lcmgcdlem  12341  lcmdvds  12343  cncongr2  12368  exprmfct  12402  pceu  12560  infpnlem1  12624  isghm  13521  ringadd2  13731  metrest  14920  bj-charfunbi  15680  bj-om  15806
  Copyright terms: Public domain W3C validator