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  4557  rexxfrd  4558  elunirn  5902  onunsnss  7104  xpfi  7119  snon0  7128  genprndl  7734  genprndu  7735  addlsub  8542  letrp1  9021  peano2uz2  9580  uzind  9584  xrre  10048  xrre2  10049  flqge  10535  monoord  10740  facwordi  10995  facavg  11001  dvdsmultr1  12385  ltoddhalfle  12447  dvdsgcdb  12577  dfgcd2  12578  coprmgcdb  12653  coprmdvds2  12658  exprmfct  12703  prmdvdsfz  12704  prmfac1  12717  rpexp  12718  eulerthlemh  12796  pcpremul  12859  pcdvdsb  12886  pcprmpw2  12899  pockthlem  12922  4sqlem11  12967  lgsne0  15760  gausslemma2dlem1a  15780  gausslemma2dlem2  15784  lgseisenlem1  15792  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2lem1  15803  lgsquad2lem2  15804