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

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  433  mpan2i  435  ralxfrd  4606  rexxfrd  4607  elunirn  5966  onunsnss  7218  xpfi  7233  snon0  7243  genprndl  7882  genprndu  7883  addlsub  8690  letrp1  9172  peano2uz2  9736  uzind  9740  xrre  10205  xrre2  10206  flqge  10700  monoord  10905  facwordi  11161  facavg  11167  dvdsmultr1  12581  ltoddhalfle  12643  dvdsgcdb  12773  dfgcd2  12774  coprmgcdb  12849  coprmdvds2  12854  exprmfct  12899  prmdvdsfz  12900  prmfac1  12913  rpexp  12914  eulerthlemh  12992  pcpremul  13055  pcdvdsb  13082  pcprmpw2  13095  pockthlem  13118  4sqlem11  13163  lgsne0  16140  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  lgseisenlem1  16172  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2lem1  16183  lgsquad2lem2  16184