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  4462  rexxfrd  4463  elunirn  5766  onunsnss  6915  xpfi  6928  snon0  6934  genprndl  7519  genprndu  7520  addlsub  8326  letrp1  8804  peano2uz2  9359  uzind  9363  xrre  9819  xrre2  9820  flqge  10281  monoord  10475  facwordi  10719  facavg  10725  dvdsmultr1  11837  ltoddhalfle  11897  dvdsgcdb  12013  dfgcd2  12014  coprmgcdb  12087  coprmdvds2  12092  exprmfct  12137  prmdvdsfz  12138  prmfac1  12151  rpexp  12152  eulerthlemh  12230  pcpremul  12292  pcdvdsb  12318  pcprmpw2  12331  pockthlem  12353  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421