Theorem mp3an2 1315

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	⊢ 𝜓
mp3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 ⊢ 𝜓
2		mp3an2.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1193	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 432	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  mp3anl2  1322  ordin  4363  ordsuc  4540  omv  6423  oeiv  6424  omv2  6433  1idprl  7531  muladd11  8031  negsub  8146  subneg  8147  ltaddneg  8322  muleqadd  8565  diveqap1  8601  conjmulap  8625  nnsub  8896  addltmul  9093  zltp1le  9245  gtndiv  9286  eluzp1m1  9489  xnn0le2is012  9802  divelunit  9938  fznatpl1  10011  flqbi2  10226  flqdiv  10256  frecfzen2  10362  nn0ennn  10368  faclbnd3  10656  shftfvalg  10760  ovshftex  10761  shftfval  10763  abs2dif  11048  cos2t  11691  sin01gt0  11702  cos01gt0  11703  demoivre  11713  demoivreALT  11714  omeo  11835  gcd0id  11912  sqgcd  11962  isprm3  12050  eulerthlemth  12164  pczpre  12229  pcrec  12240  setscom  12434  setsslid  12444  setsslnid  12445  abssinper  13417  lgs1  13595