Theorem mp3an 1378

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  vtocl3  2879  raltp  3766  rextp  3767  ordtriexmidlem  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsoexmid  4711  funopg  5414  ftp  5903  caovass  6253  caovdi  6272  mptexw  6346  ofmres  6373  mpofvexi  6446  mpoexw  6453  dmtpos  6531  rntpos  6532  dftpos3  6537  tpostpos  6539  mapsnen  7104  xpcomen  7129  mapxpen  7152  xpmapenlem  7153  unfiexmid  7229  1lt2pi  7713  1lt2nq  7779  halfnqq  7783  m1p1sr  8133  m1m1sr  8134  suplocsrlempr  8180  addassi  8340  mulassi  8341  adddii  8342  adddiri  8343  lttri  8437  lelttri  8438  ltletri  8439  letri  8440  mul12i  8479  mul32i  8480  add12i  8496  add32i  8497  addcani  8515  addcan2i  8516  subaddi  8620  subadd2i  8621  subsub23i  8623  addsubassi  8624  addsubi  8625  subcani  8626  subcan2i  8627  pnncani  8628  subdii  8741  subdiri  8742  ltadd2i  8755  ltadd1i  8837  leadd1i  8838  leadd2i  8839  ltsubaddi  8840  lesubaddi  8841  ltsubadd2i  8842  lesubadd2i  8843  ltaddsubi  8844  gtapii  8970  mulcanapi  9003  divclapi  9092  divcanap2i  9093  divcanap1i  9094  divrecapi  9095  divcanap3i  9096  divcanap4i  9097  divassapi  9106  divdirapi  9107  div23api  9108  div11api  9109  sup3exmid  9295  1mhlfehlf  9534  halfpm6th  9536  3halfnz  9754  addex  10069  mulex  10070  unirnioo  10392  nnenom  10892  inftonninf  10900  m1expcl2  11019  i4  11100  expnass  11103  bcn1  11218  hashinfom  11239  abs3difi  11945  0.999...  12313  ef01bndlem  12548  cos1bnd  12551  cos2bnd  12552  sin4lt0  12559  3dvdsdec  12657  3dvds2dec  12658  ndvdsi  12725  flodddiv4  12728  3lcm2e6woprm  12889  6lcm4e12  12890  3prm  12931  dec2dvds  13219  modxai  13224  gcdi  13229  numexp2x  13234  2exp5  13241  2exp11  13245  ballotfilem2  13286  ballotfilemafi  13296  ballotfilembfi  13297  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemth  13339  znnen  13347  ennnfonelem1  13356  prminf  13404  topnfn  13657  prdsvallem  13680  prdsval  14280  fnmgp  14326  rhmex  14573  rmodislmodlem  14796  rmodislmod  14797  cnfldstr  15004  zring0  15044  fnpsr  15160  mplvalcoe  15206  fnmpl  15209  xmetunirn  15584  tgioo  15780  tgqioo  15781  addcncntoplem  15787  expcncf  15835  dveflem  15952  dvef  15953  efcn  15994  sinhalfpilem  16018  sincosq1lem  16052  sincosq4sgn  16056  cosq23lt0  16060  coseq00topi  16062  coseq0negpitopi  16063  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  pigt3  16071  cos02pilt1  16079  cos0pilt1  16080  2logb9irr  16207  2logb3irr  16209  2logb9irrALT  16210  sqrt2cxp2logb9e3  16211  2irrexpq  16212  2logb9irrap  16213  2irrexpqap  16214  log2tlbndlog2  16220  log2ublem1  16221  log2ublem2  16222  log2ublog2  16224  1sgm2ppw  16289  ppiqub  16293  bclbnd  16307  bposlem8  16318  lgseisenlem1  16394  lgseisenlem2  16395  lgsquadlem1  16401  upgr2wlkdc  16823  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem5  16938  ex-fl  16944  ex-exp  16946  repiecelem  17280  repiecege0  17282  trilpolemeq1  17296