Theorem mp3an 1298

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

Syntax hints:   → wi 4   ∧ w3a 945

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

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

This theorem is referenced by:  vtocl3  2713  raltp  3546  rextp  3547  ordtriexmidlem  4395  ordtri2or2exmidlem  4401  onsucelsucexmidlem  4404  ordsoexmid  4437  funopg  5115  ftp  5559  caovass  5885  caovdi  5904  ofmres  5988  mpofvexi  6058  dmtpos  6107  rntpos  6108  dftpos3  6113  tpostpos  6115  mapsnen  6659  xpcomen  6674  mapxpen  6695  xpmapenlem  6696  unfiexmid  6759  1lt2pi  7096  1lt2nq  7162  halfnqq  7166  m1p1sr  7503  m1m1sr  7504  addassi  7698  mulassi  7699  adddii  7700  adddiri  7701  lttri  7791  lelttri  7792  ltletri  7793  letri  7794  mul12i  7831  mul32i  7832  add12i  7848  add32i  7849  addcani  7867  addcan2i  7868  subaddi  7972  subadd2i  7973  subsub23i  7975  addsubassi  7976  addsubi  7977  subcani  7978  subcan2i  7979  pnncani  7980  subdii  8088  subdiri  8089  ltadd2i  8101  ltadd1i  8183  leadd1i  8184  leadd2i  8185  ltsubaddi  8186  lesubaddi  8187  ltsubadd2i  8188  lesubadd2i  8189  ltaddsubi  8190  gtapii  8313  mulcanapi  8341  divclapi  8427  divcanap2i  8428  divcanap1i  8429  divrecapi  8430  divcanap3i  8431  divcanap4i  8432  divassapi  8441  divdirapi  8442  div23api  8443  div11api  8444  sup3exmid  8625  1mhlfehlf  8842  halfpm6th  8844  3halfnz  9052  unirnioo  9649  nnenom  10100  inftonninf  10107  m1expcl2  10208  i4  10288  expnass  10291  bcn1  10397  hashinfom  10417  abs3difi  10820  0.999...  11182  ef01bndlem  11314  cos1bnd  11317  cos2bnd  11318  sin4lt0  11324  3dvdsdec  11410  3dvds2dec  11411  ndvdsi  11478  flodddiv4  11479  3lcm2e6woprm  11613  6lcm4e12  11614  3prm  11655  znnen  11756  ennnfonelem1  11765  topnfn  11968  xmetunirn  12347  tgioo  12532  tgqioo  12533  addcncntoplem  12537  expcncf  12578  ex-fl  12630  ex-exp  12632  trilpolemeq1  12925