ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantrd Structured version   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  639  prlem1  879  equveli  1639  elssabg  3893  suctr  4124  fvun1  5182  opabbrex  5491  poxp  5794  tposfo2  5823  1idprl  6565  1idpru  6566  uzind  8105  xrlttr  8466  fzen  8657  fz0fzelfz0  8734  bj-om  9371
  Copyright terms: Public domain W3C validator