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

Theorem mpan2d 412
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mpan2d.1 (𝜑𝜒)
mpan2d.2 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
mpan2d (𝜑 → (𝜓𝜃))

Proof of Theorem mpan2d
StepHypRef Expression
1 mpan2d.1 . 2 (𝜑𝜒)
2 mpan2d.2 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 249 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 41 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mpand  413  mpan2i  415  ralxfrd  4222  rexxfrd  4223  elunirn  5433  onunsnss  6386  snon0  6387  genprndl  6677  genprndu  6678  addlsub  7440  letrp1  7889  peano2uz2  8404  uzind  8408  xrre  8834  xrre2  8835  flqge  9232  monoord  9399  facwordi  9608  facavg  9614  dvdsmultr1  10145  ltoddhalfle  10205
  Copyright terms: Public domain W3C validator