Theorem mp3an 1348

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
mp3an.1	⊢ 𝜑
mp3an.2	⊢ 𝜓
mp3an.3	⊢ 𝜒
mp3an.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an	⊢ 𝜃

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 ⊢ 𝜓
2		mp3an.3	. 2 ⊢ 𝜒
3		mp3an.1	. . 3 ⊢ 𝜑
4		mp3an.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
5	3, 4	mp3an1 1335	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 426	1 ⊢ 𝜃

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  vtocl3  2820  raltp  3680  rextp  3681  ordtriexmidlem  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsoexmid  4599  funopg  5293  ftp  5750  caovass  6088  caovdi  6107  mptexw  6179  ofmres  6202  mpofvexi  6273  mpoexw  6280  dmtpos  6323  rntpos  6324  dftpos3  6329  tpostpos  6331  mapsnen  6879  xpcomen  6895  mapxpen  6918  xpmapenlem  6919  unfiexmid  6988  1lt2pi  7426  1lt2nq  7492  halfnqq  7496  m1p1sr  7846  m1m1sr  7847  suplocsrlempr  7893  addassi  8053  mulassi  8054  adddii  8055  adddiri  8056  lttri  8150  lelttri  8151  ltletri  8152  letri  8153  mul12i  8191  mul32i  8192  add12i  8208  add32i  8209  addcani  8227  addcan2i  8228  subaddi  8332  subadd2i  8333  subsub23i  8335  addsubassi  8336  addsubi  8337  subcani  8338  subcan2i  8339  pnncani  8340  subdii  8452  subdiri  8453  ltadd2i  8466  ltadd1i  8548  leadd1i  8549  leadd2i  8550  ltsubaddi  8551  lesubaddi  8552  ltsubadd2i  8553  lesubadd2i  8554  ltaddsubi  8555  gtapii  8680  mulcanapi  8713  divclapi  8800  divcanap2i  8801  divcanap1i  8802  divrecapi  8803  divcanap3i  8804  divcanap4i  8805  divassapi  8814  divdirapi  8815  div23api  8816  div11api  8817  sup3exmid  9003  1mhlfehlf  9228  halfpm6th  9230  3halfnz  9442  addex  9745  mulex  9746  unirnioo  10067  nnenom  10545  inftonninf  10553  m1expcl2  10672  i4  10753  expnass  10756  bcn1  10869  hashinfom  10889  abs3difi  11340  0.999...  11705  ef01bndlem  11940  cos1bnd  11943  cos2bnd  11944  sin4lt0  11951  3dvdsdec  12049  3dvds2dec  12050  ndvdsi  12117  flodddiv4  12120  3lcm2e6woprm  12281  6lcm4e12  12282  3prm  12323  dec2dvds  12607  modxai  12612  gcdi  12616  numexp2x  12621  2exp5  12628  2exp11  12632  znnen  12642  ennnfonelem1  12651  prminf  12699  topnfn  12948  prdsvallem  12976  prdsval  12977  fnmgp  13556  rhmex  13791  rmodislmodlem  13984  rmodislmod  13985  cnfldstr  14192  zring0  14234  fnpsr  14301  mplvalcoe  14324  fnmpl  14327  xmetunirn  14702  tgioo  14898  tgqioo  14899  addcncntoplem  14905  expcncf  14953  dveflem  15070  dvef  15071  efcn  15112  sinhalfpilem  15135  sincosq1lem  15169  sincosq4sgn  15173  cosq23lt0  15177  coseq00topi  15179  coseq0negpitopi  15180  tangtx  15182  sincos4thpi  15184  sincos6thpi  15186  pigt3  15188  cos02pilt1  15195  cos0pilt1  15196  2logb9irr  15315  2logb3irr  15317  2logb9irrALT  15318  sqrt2cxp2logb9e3  15319  2irrexpq  15320  2logb9irrap  15321  2irrexpqap  15322  1sgm2ppw  15339  lgseisenlem1  15419  lgseisenlem2  15420  lgsquadlem1  15426  ex-fl  15479  ex-exp  15481  trilpolemeq1  15797