Theorem mpan2d 432

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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpand  433  mpan2i  435  ralxfrd  4610  rexxfrd  4611  elunirn  5975  onunsnss  7230  xpfi  7245  snon0  7255  genprndl  7895  genprndu  7896  addlsub  8704  letrp1  9187  peano2uz2  9764  uzind  9768  xrre  10239  xrre2  10240  flqge  10736  flapge  10737  monoord  10943  facwordi  11200  facavg  11206  dvdsmultr1  12623  ltoddhalfle  12685  dvdsgcdb  12815  dfgcd2  12816  coprmgcdb  12891  coprmdvds2  12896  exprmfct  12942  prmdvdsfz  12943  prmfac1  12956  rpexp  12957  eulerthlemh  13038  pcpremul  13101  pcdvdsb  13128  pcprmpw2  13141  pockthlem  13164  4sqlem11  13209  chtqub  16329  bposlem3  16346  lgsne0  16395  gausslemma2dlem1a  16415  gausslemma2dlem2  16419  lgseisenlem1  16427  lgseisenlem2  16428  lgsquadlem1  16434  lgsquadlem2  16435  lgsquadlem3  16436  lgsquad2lem1  16438  lgsquad2lem2  16439