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  4588  rexxfrd  4589  elunirn  5945  onunsnss  7190  xpfi  7205  snon0  7215  genprndl  7852  genprndu  7853  addlsub  8660  letrp1  9142  peano2uz2  9706  uzind  9710  xrre  10175  xrre2  10176  flqge  10669  monoord  10874  facwordi  11130  facavg  11136  dvdsmultr1  12546  ltoddhalfle  12608  dvdsgcdb  12738  dfgcd2  12739  coprmgcdb  12814  coprmdvds2  12819  exprmfct  12864  prmdvdsfz  12865  prmfac1  12878  rpexp  12879  eulerthlemh  12957  pcpremul  13020  pcdvdsb  13047  pcprmpw2  13060  pockthlem  13083  4sqlem11  13128  lgsne0  16041  gausslemma2dlem1a  16061  gausslemma2dlem2  16065  lgseisenlem1  16073  lgseisenlem2  16074  lgsquadlem1  16080  lgsquadlem2  16081  lgsquadlem3  16082  lgsquad2lem1  16084  lgsquad2lem2  16085