Theorem mpan2d 424

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 256	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpid 42	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mpand  425  mpan2i  427  ralxfrd  4378  rexxfrd  4379  elunirn  5660  onunsnss  6798  xpfi  6811  snon0  6817  genprndl  7322  genprndu  7323  addlsub  8125  letrp1  8599  peano2uz2  9151  uzind  9155  xrre  9596  xrre2  9597  flqge  10048  monoord  10242  facwordi  10479  facavg  10485  dvdsmultr1  11520  ltoddhalfle  11579  dvdsgcdb  11690  dfgcd2  11691  coprmgcdb  11758  coprmdvds2  11763  exprmfct  11807  prmdvdsfz  11808  prmfac1  11819  rpexp  11820