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  4498  rexxfrd  4499  elunirn  5816  onunsnss  6987  xpfi  7002  snon0  7010  genprndl  7607  genprndu  7608  addlsub  8415  letrp1  8894  peano2uz2  9452  uzind  9456  xrre  9914  xrre2  9915  flqge  10391  monoord  10596  facwordi  10851  facavg  10857  dvdsmultr1  12015  ltoddhalfle  12077  dvdsgcdb  12207  dfgcd2  12208  coprmgcdb  12283  coprmdvds2  12288  exprmfct  12333  prmdvdsfz  12334  prmfac1  12347  rpexp  12348  eulerthlemh  12426  pcpremul  12489  pcdvdsb  12516  pcprmpw2  12529  pockthlem  12552  4sqlem11  12597  lgsne0  15387  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  lgseisenlem1  15419  lgseisenlem2  15420  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  lgsquad2lem2  15431