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  4353  rexxfrd  4354  elunirn  5635  onunsnss  6773  xpfi  6786  snon0  6792  genprndl  7297  genprndu  7298  addlsub  8100  letrp1  8574  peano2uz2  9126  uzind  9130  xrre  9571  xrre2  9572  flqge  10023  monoord  10217  facwordi  10454  facavg  10460  dvdsmultr1  11458  ltoddhalfle  11517  dvdsgcdb  11628  dfgcd2  11629  coprmgcdb  11696  coprmdvds2  11701  exprmfct  11745  prmdvdsfz  11746  prmfac1  11757  rpexp  11758
  Copyright terms: Public domain W3C validator