Theorem mpan2d 432

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  433  mpan2i  435  ralxfrd  4606  rexxfrd  4607  elunirn  5965  onunsnss  7217  xpfi  7232  snon0  7242  genprndl  7881  genprndu  7882  addlsub  8689  letrp1  9171  peano2uz2  9735  uzind  9739  xrre  10204  xrre2  10205  flqge  10698  monoord  10903  facwordi  11159  facavg  11165  dvdsmultr1  12579  ltoddhalfle  12641  dvdsgcdb  12771  dfgcd2  12772  coprmgcdb  12847  coprmdvds2  12852  exprmfct  12897  prmdvdsfz  12898  prmfac1  12911  rpexp  12912  eulerthlemh  12990  pcpremul  13053  pcdvdsb  13080  pcprmpw2  13093  pockthlem  13116  4sqlem11  13161  lgsne0  16074  gausslemma2dlem1a  16094  gausslemma2dlem2  16098  lgseisenlem1  16106  lgseisenlem2  16107  lgsquadlem1  16113  lgsquadlem2  16114  lgsquadlem3  16115  lgsquad2lem1  16117  lgsquad2lem2  16118