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  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