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

Theorem mpan2d 424
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 256 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 42 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mpand  425  mpan2i  427  ralxfrd  4383  rexxfrd  4384  elunirn  5667  onunsnss  6805  xpfi  6818  snon0  6824  genprndl  7343  genprndu  7344  addlsub  8146  letrp1  8620  peano2uz2  9172  uzind  9176  xrre  9617  xrre2  9618  flqge  10069  monoord  10263  facwordi  10500  facavg  10506  dvdsmultr1  11544  ltoddhalfle  11603  dvdsgcdb  11714  dfgcd2  11715  coprmgcdb  11782  coprmdvds2  11787  exprmfct  11831  prmdvdsfz  11832  prmfac1  11843  rpexp  11844
  Copyright terms: Public domain W3C validator