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  4559  rexxfrd  4560  elunirn  5907  onunsnss  7109  xpfi  7124  snon0  7134  genprndl  7741  genprndu  7742  addlsub  8549  letrp1  9028  peano2uz2  9587  uzind  9591  xrre  10055  xrre2  10056  flqge  10543  monoord  10748  facwordi  11003  facavg  11009  dvdsmultr1  12397  ltoddhalfle  12459  dvdsgcdb  12589  dfgcd2  12590  coprmgcdb  12665  coprmdvds2  12670  exprmfct  12715  prmdvdsfz  12716  prmfac1  12729  rpexp  12730  eulerthlemh  12808  pcpremul  12871  pcdvdsb  12898  pcprmpw2  12911  pockthlem  12934  4sqlem11  12979  lgsne0  15773  gausslemma2dlem1a  15793  gausslemma2dlem2  15797  lgseisenlem1  15805  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem1  15816  lgsquad2lem2  15817