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  4530  rexxfrd  4531  elunirn  5863  onunsnss  7047  xpfi  7062  snon0  7070  genprndl  7676  genprndu  7677  addlsub  8484  letrp1  8963  peano2uz2  9522  uzind  9526  xrre  9984  xrre2  9985  flqge  10469  monoord  10674  facwordi  10929  facavg  10935  dvdsmultr1  12308  ltoddhalfle  12370  dvdsgcdb  12500  dfgcd2  12501  coprmgcdb  12576  coprmdvds2  12581  exprmfct  12626  prmdvdsfz  12627  prmfac1  12640  rpexp  12641  eulerthlemh  12719  pcpremul  12782  pcdvdsb  12809  pcprmpw2  12822  pockthlem  12845  4sqlem11  12890  lgsne0  15682  gausslemma2dlem1a  15702  gausslemma2dlem2  15706  lgseisenlem1  15714  lgseisenlem2  15715  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2lem1  15725  lgsquad2lem2  15726