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

Theorem mpan2d 428
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 258 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpid 42 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  mpand  429  mpan2i  431  ralxfrd  4480  rexxfrd  4481  elunirn  5788  onunsnss  6946  xpfi  6959  snon0  6966  genprndl  7551  genprndu  7552  addlsub  8358  letrp1  8836  peano2uz2  9391  uzind  9395  xrre  9852  xrre2  9853  flqge  10315  monoord  10509  facwordi  10755  facavg  10761  dvdsmultr1  11873  ltoddhalfle  11933  dvdsgcdb  12049  dfgcd2  12050  coprmgcdb  12123  coprmdvds2  12128  exprmfct  12173  prmdvdsfz  12174  prmfac1  12187  rpexp  12188  eulerthlemh  12266  pcpremul  12328  pcdvdsb  12355  pcprmpw2  12368  pockthlem  12391  4sqlem11  12436  lgsne0  14917  lgseisenlem1  14928  lgseisenlem2  14929
  Copyright terms: Public domain W3C validator