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

Theorem mpan2d 420
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 255 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 42 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107
This theorem is referenced by:  mpand  421  mpan2i  423  ralxfrd  4312  rexxfrd  4313  elunirn  5583  onunsnss  6707  xpfi  6720  snon0  6725  genprndl  7177  genprndu  7178  addlsub  7945  letrp1  8406  peano2uz2  8952  uzind  8956  xrre  9386  xrre2  9387  flqge  9838  monoord  10042  facwordi  10279  facavg  10285  dvdsmultr1  11277  ltoddhalfle  11336  dvdsgcdb  11445  dfgcd2  11446  coprmgcdb  11513  coprmdvds2  11518  exprmfct  11562  prmdvdsfz  11563  prmfac1  11574  rpexp  11575
  Copyright terms: Public domain W3C validator