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

Step	Hyp	Ref	Expression
1		mpan2d.1	. 2 ⊢ (𝜑 → 𝜒)
2		mpan2d.2	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 258	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpid 42	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  4554  rexxfrd  4555  elunirn  5899  onunsnss  7095  xpfi  7110  snon0  7118  genprndl  7724  genprndu  7725  addlsub  8532  letrp1  9011  peano2uz2  9570  uzind  9574  xrre  10033  xrre2  10034  flqge  10519  monoord  10724  facwordi  10979  facavg  10985  dvdsmultr1  12363  ltoddhalfle  12425  dvdsgcdb  12555  dfgcd2  12556  coprmgcdb  12631  coprmdvds2  12636  exprmfct  12681  prmdvdsfz  12682  prmfac1  12695  rpexp  12696  eulerthlemh  12774  pcpremul  12837  pcdvdsb  12864  pcprmpw2  12877  pockthlem  12900  4sqlem11  12945  lgsne0  15738  gausslemma2dlem1a  15758  gausslemma2dlem2  15762  lgseisenlem1  15770  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2lem1  15781  lgsquad2lem2  15782