Theorem mp3an1 1324

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

Hypotheses

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

Assertion

Ref	Expression
mp3an1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ 𝜑
2		mp3an1.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expb 1204	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 424	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  mp3an12  1327  mp3an1i  1330  mp3anl1  1331  mp3an  1337  mp3an2i  1342  mp3an3an  1343  tfrlem9  6319  rdgexgg  6378  oaexg  6448  omexg  6451  oeiexg  6453  oav2  6463  nnaordex  6528  mulidnq  7387  1idpru  7589  addgt0sr  7773  muladd11  8089  cnegex  8134  negsubdi  8212  renegcl  8217  mulneg1  8351  ltaddpos  8408  addge01  8428  rimul  8541  recclap  8635  recidap  8642  recidap2  8643  recdivap2  8681  divdiv23apzi  8721  ltmul12a  8816  lemul12a  8818  mulgt1  8819  ltmulgt11  8820  gt0div  8826  ge0div  8827  ltdiv23i  8882  8th4div3  9137  gtndiv  9347  nn0ind  9366  fnn0ind  9368  xrre2  9820  ioorebasg  9974  fzen  10042  elfz0ubfz0  10124  expubnd  10576  le2sq2  10595  bernneq  10640  expnbnd  10643  faclbnd6  10723  bccl  10746  hashfacen  10815  shftfval  10829  mulreap  10872  caucvgrelemrec  10987  binom1p  11492  efi4p  11724  sinadd  11743  cosadd  11744  cos2t  11757  cos2tsin  11758  absefib  11777  efieq1re  11778  demoivreALT  11780  odd2np1  11877  opoe  11899  omoe  11900  opeo  11901  omeo  11902  gcdadd  11985  gcdmultiple  12020  algcvgblem  12048  algcvga  12050  isprm3  12117  coprm  12143  1arith2  12365  cnfldneg  13437  cnfldmulg  13440  cnfldexp  13441  zringmulg  13458  zringsubgval  13465  bl2ioo  14012  ioo2blex  14014  sinperlem  14199  logge0  14271  lgsdir2  14404  1lgs  14414