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  7229  xpfi  7244  snon0  7254  genprndl  7895  genprndu  7896  addlsub  8704  letrp1  9187  peano2uz2  9765  uzind  9769  xrre  10240  xrre2  10241  flqge  10737  flapge  10738  monoord  10944  facwordi  11201  facavg  11207  dvdsmultr1  12624  ltoddhalfle  12686  dvdsgcdb  12816  dfgcd2  12817  coprmgcdb  12892  coprmdvds2  12897  exprmfct  12943  prmdvdsfz  12944  prmfac1  12957  rpexp  12958  eulerthlemh  13039  pcpremul  13102  pcdvdsb  13129  pcprmpw2  13142  pockthlem  13165  4sqlem11  13210  chtqub  16308  bposlem3  16325  lgsne0  16374  gausslemma2dlem1a  16394  gausslemma2dlem2  16398  lgseisenlem1  16406  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad2lem1  16417  lgsquad2lem2  16418