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  4463  rexxfrd  4464  elunirn  5767  onunsnss  6916  xpfi  6929  snon0  6935  genprndl  7520  genprndu  7521  addlsub  8327  letrp1  8805  peano2uz2  9360  uzind  9364  xrre  9820  xrre2  9821  flqge  10282  monoord  10476  facwordi  10720  facavg  10726  dvdsmultr1  11838  ltoddhalfle  11898  dvdsgcdb  12014  dfgcd2  12015  coprmgcdb  12088  coprmdvds2  12093  exprmfct  12138  prmdvdsfz  12139  prmfac1  12152  rpexp  12153  eulerthlemh  12231  pcpremul  12293  pcdvdsb  12319  pcprmpw2  12332  pockthlem  12354  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454