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  6566  1idpru  6567  uzind  8125  xrlttr  8486  fzen  8677  fz0fzelfz0  8754  bj-om  9396
  Copyright terms: Public domain W3C validator