ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantrd GIF version

Theorem adantrd 273
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 107 . 2 ((𝜓𝜃) → 𝜓)
2 adantrd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 32 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem is referenced by:  syldan  276  jaoa  673  prlem1  917  equveli  1686  elssabg  3958  suctr  4221  fvun1  5327  opabbrex  5644  poxp  5948  tposfo2  5980  1idprl  7086  1idpru  7087  uzind  8783  xrlttr  9190  fzen  9382  fz0fzelfz0  9459  zeqzmulgcd  10829  lcmgcdlem  10926  lcmdvds  10928  cncongr2  10953  exprmfct  10986  bj-om  11262
  Copyright terms: Public domain W3C validator