Theorem mpan2d 420

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpand  421  mpan2i  423  ralxfrd  4312  rexxfrd  4313  elunirn  5583  onunsnss  6707  xpfi  6720  snon0  6725  genprndl  7177  genprndu  7178  addlsub  7945  letrp1  8406  peano2uz2  8952  uzind  8956  xrre  9386  xrre2  9387  flqge  9838  monoord  10042  facwordi  10279  facavg  10285  dvdsmultr1  11277  ltoddhalfle  11336  dvdsgcdb  11445  dfgcd2  11446  coprmgcdb  11513  coprmdvds2  11518  exprmfct  11562  prmdvdsfz  11563  prmfac1  11574  rpexp  11575