Theorem mpan2d 426

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  427  mpan2i  429  ralxfrd  4447  rexxfrd  4448  elunirn  5745  onunsnss  6894  xpfi  6907  snon0  6913  genprndl  7483  genprndu  7484  addlsub  8289  letrp1  8764  peano2uz2  9319  uzind  9323  xrre  9777  xrre2  9778  flqge  10238  monoord  10432  facwordi  10674  facavg  10680  dvdsmultr1  11793  ltoddhalfle  11852  dvdsgcdb  11968  dfgcd2  11969  coprmgcdb  12042  coprmdvds2  12047  exprmfct  12092  prmdvdsfz  12093  prmfac1  12106  rpexp  12107  eulerthlemh  12185  pcpremul  12247  pcdvdsb  12273  pcprmpw2  12286  pockthlem  12308  lgsne0  13733