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  974  equveli  1769  elssabg  4160  suctr  4433  fvun1  5595  opabbrex  5932  poxp  6246  tposfo2  6281  1idprl  7602  1idpru  7603  uzind  9377  xrlttr  9808  fzen  10056  fz0fzelfz0  10140  fisumss  11413  fprodssdc  11611  zeqzmulgcd  11984  lcmgcdlem  12090  lcmdvds  12092  cncongr2  12117  exprmfct  12151  pceu  12308  infpnlem1  12370  ringadd2  13264  metrest  14233  bj-charfunbi  14790  bj-om  14916
  Copyright terms: Public domain W3C validator