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  4456  rexxfrd  4457  elunirn  5757  onunsnss  6906  xpfi  6919  snon0  6925  genprndl  7495  genprndu  7496  addlsub  8301  letrp1  8776  peano2uz2  9331  uzind  9335  xrre  9789  xrre2  9790  flqge  10250  monoord  10444  facwordi  10686  facavg  10692  dvdsmultr1  11804  ltoddhalfle  11863  dvdsgcdb  11979  dfgcd2  11980  coprmgcdb  12053  coprmdvds2  12058  exprmfct  12103  prmdvdsfz  12104  prmfac1  12117  rpexp  12118  eulerthlemh  12196  pcpremul  12258  pcdvdsb  12284  pcprmpw2  12297  pockthlem  12319  lgsne0  13990