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  4608  rexxfrd  4609  elunirn  5972  onunsnss  7224  xpfi  7239  snon0  7249  genprndl  7888  genprndu  7889  addlsub  8696  letrp1  9179  peano2uz2  9755  uzind  9759  xrre  10224  xrre2  10225  flqge  10719  monoord  10924  facwordi  11180  facavg  11186  dvdsmultr1  12600  ltoddhalfle  12662  dvdsgcdb  12792  dfgcd2  12793  coprmgcdb  12868  coprmdvds2  12873  exprmfct  12918  prmdvdsfz  12919  prmfac1  12932  rpexp  12933  eulerthlemh  13011  pcpremul  13074  pcdvdsb  13101  pcprmpw2  13114  pockthlem  13137  4sqlem11  13182  lgsne0  16169  gausslemma2dlem1a  16189  gausslemma2dlem2  16193  lgseisenlem1  16201  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2lem1  16212  lgsquad2lem2  16213