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  4528  rexxfrd  4529  elunirn  5860  onunsnss  7042  xpfi  7057  snon0  7065  genprndl  7671  genprndu  7672  addlsub  8479  letrp1  8958  peano2uz2  9517  uzind  9521  xrre  9979  xrre2  9980  flqge  10464  monoord  10669  facwordi  10924  facavg  10930  dvdsmultr1  12303  ltoddhalfle  12365  dvdsgcdb  12495  dfgcd2  12496  coprmgcdb  12571  coprmdvds2  12576  exprmfct  12621  prmdvdsfz  12622  prmfac1  12635  rpexp  12636  eulerthlemh  12714  pcpremul  12777  pcdvdsb  12804  pcprmpw2  12817  pockthlem  12840  4sqlem11  12885  lgsne0  15676  gausslemma2dlem1a  15696  gausslemma2dlem2  15700  lgseisenlem1  15708  lgseisenlem2  15709  lgsquadlem1  15715  lgsquadlem2  15716  lgsquadlem3  15717  lgsquad2lem1  15719  lgsquad2lem2  15720