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  4565  rexxfrd  4566  elunirn  5917  onunsnss  7152  xpfi  7167  snon0  7177  genprndl  7784  genprndu  7785  addlsub  8592  letrp1  9071  peano2uz2  9630  uzind  9634  xrre  10098  xrre2  10099  flqge  10586  monoord  10791  facwordi  11046  facavg  11052  dvdsmultr1  12453  ltoddhalfle  12515  dvdsgcdb  12645  dfgcd2  12646  coprmgcdb  12721  coprmdvds2  12726  exprmfct  12771  prmdvdsfz  12772  prmfac1  12785  rpexp  12786  eulerthlemh  12864  pcpremul  12927  pcdvdsb  12954  pcprmpw2  12967  pockthlem  12990  4sqlem11  13035  lgsne0  15837  gausslemma2dlem1a  15857  gausslemma2dlem2  15861  lgseisenlem1  15869  lgseisenlem2  15870  lgsquadlem1  15876  lgsquadlem2  15877  lgsquadlem3  15878  lgsquad2lem1  15880  lgsquad2lem2  15881