Theorem mp3an 1337

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 1324	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 426	1 ⊢ 𝜃

Syntax hints:   → wi 4   ∧ 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:  vtocl3  2791  raltp  3646  rextp  3647  ordtriexmidlem  4512  ordtri2or2exmidlem  4519  onsucelsucexmidlem  4522  ordsoexmid  4555  funopg  5242  ftp  5693  caovass  6025  caovdi  6044  mptexw  6104  ofmres  6127  mpofvexi  6197  mpoexw  6204  dmtpos  6247  rntpos  6248  dftpos3  6253  tpostpos  6255  mapsnen  6801  xpcomen  6817  mapxpen  6838  xpmapenlem  6839  unfiexmid  6907  1lt2pi  7314  1lt2nq  7380  halfnqq  7384  m1p1sr  7734  m1m1sr  7735  suplocsrlempr  7781  addassi  7940  mulassi  7941  adddii  7942  adddiri  7943  lttri  8036  lelttri  8037  ltletri  8038  letri  8039  mul12i  8077  mul32i  8078  add12i  8094  add32i  8095  addcani  8113  addcan2i  8114  subaddi  8218  subadd2i  8219  subsub23i  8221  addsubassi  8222  addsubi  8223  subcani  8224  subcan2i  8225  pnncani  8226  subdii  8338  subdiri  8339  ltadd2i  8351  ltadd1i  8433  leadd1i  8434  leadd2i  8435  ltsubaddi  8436  lesubaddi  8437  ltsubadd2i  8438  lesubadd2i  8439  ltaddsubi  8440  gtapii  8565  mulcanapi  8597  divclapi  8684  divcanap2i  8685  divcanap1i  8686  divrecapi  8687  divcanap3i  8688  divcanap4i  8689  divassapi  8698  divdirapi  8699  div23api  8700  div11api  8701  sup3exmid  8887  1mhlfehlf  9110  halfpm6th  9112  3halfnz  9323  unirnioo  9944  nnenom  10404  inftonninf  10411  m1expcl2  10512  i4  10592  expnass  10595  bcn1  10706  hashinfom  10726  abs3difi  11133  0.999...  11497  ef01bndlem  11732  cos1bnd  11735  cos2bnd  11736  sin4lt0  11742  3dvdsdec  11837  3dvds2dec  11838  ndvdsi  11905  flodddiv4  11906  3lcm2e6woprm  12053  6lcm4e12  12054  3prm  12095  znnen  12366  ennnfonelem1  12375  prminf  12423  topnfn  12615  fnmgp  12930  xmetunirn  13429  tgioo  13617  tgqioo  13618  addcncntoplem  13622  expcncf  13663  dveflem  13758  dvef  13759  efcn  13760  sinhalfpilem  13783  sincosq1lem  13817  sincosq4sgn  13821  cosq23lt0  13825  coseq00topi  13827  coseq0negpitopi  13828  tangtx  13830  sincos4thpi  13832  sincos6thpi  13834  pigt3  13836  cos02pilt1  13843  cos0pilt1  13844  2logb9irr  13960  2logb3irr  13962  2logb9irrALT  13963  sqrt2cxp2logb9e3  13964  2irrexpq  13965  2logb9irrap  13966  2irrexpqap  13967  ex-fl  14037  ex-exp  14039  trilpolemeq1  14349