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  4513  rexxfrd  4514  elunirn  5842  onunsnss  7021  xpfi  7036  snon0  7044  genprndl  7641  genprndu  7642  addlsub  8449  letrp1  8928  peano2uz2  9487  uzind  9491  xrre  9949  xrre2  9950  flqge  10432  monoord  10637  facwordi  10892  facavg  10898  dvdsmultr1  12186  ltoddhalfle  12248  dvdsgcdb  12378  dfgcd2  12379  coprmgcdb  12454  coprmdvds2  12459  exprmfct  12504  prmdvdsfz  12505  prmfac1  12518  rpexp  12519  eulerthlemh  12597  pcpremul  12660  pcdvdsb  12687  pcprmpw2  12700  pockthlem  12723  4sqlem11  12768  lgsne0  15559  gausslemma2dlem1a  15579  gausslemma2dlem2  15583  lgseisenlem1  15591  lgseisenlem2  15592  lgsquadlem1  15598  lgsquadlem2  15599  lgsquadlem3  15600  lgsquad2lem1  15602  lgsquad2lem2  15603