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  1770  elssabg  4163  suctr  4436  fvun1  5598  opabbrex  5935  poxp  6251  tposfo2  6286  1idprl  7607  1idpru  7608  uzind  9382  xrlttr  9813  fzen  10061  fz0fzelfz0  10145  fisumss  11418  fprodssdc  11616  zeqzmulgcd  11989  lcmgcdlem  12095  lcmdvds  12097  cncongr2  12122  exprmfct  12156  pceu  12313  infpnlem1  12375  isghm  13143  ringadd2  13342  metrest  14403  bj-charfunbi  14960  bj-om  15086
  Copyright terms: Public domain W3C validator