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  2793  raltp  3649  rextp  3650  ordtriexmidlem  4518  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  ordsoexmid  4561  funopg  5250  ftp  5701  caovass  6034  caovdi  6053  mptexw  6113  ofmres  6136  mpofvexi  6206  mpoexw  6213  dmtpos  6256  rntpos  6257  dftpos3  6262  tpostpos  6264  mapsnen  6810  xpcomen  6826  mapxpen  6847  xpmapenlem  6848  unfiexmid  6916  1lt2pi  7338  1lt2nq  7404  halfnqq  7408  m1p1sr  7758  m1m1sr  7759  suplocsrlempr  7805  addassi  7964  mulassi  7965  adddii  7966  adddiri  7967  lttri  8061  lelttri  8062  ltletri  8063  letri  8064  mul12i  8102  mul32i  8103  add12i  8119  add32i  8120  addcani  8138  addcan2i  8139  subaddi  8243  subadd2i  8244  subsub23i  8246  addsubassi  8247  addsubi  8248  subcani  8249  subcan2i  8250  pnncani  8251  subdii  8363  subdiri  8364  ltadd2i  8376  ltadd1i  8458  leadd1i  8459  leadd2i  8460  ltsubaddi  8461  lesubaddi  8462  ltsubadd2i  8463  lesubadd2i  8464  ltaddsubi  8465  gtapii  8590  mulcanapi  8623  divclapi  8710  divcanap2i  8711  divcanap1i  8712  divrecapi  8713  divcanap3i  8714  divcanap4i  8715  divassapi  8724  divdirapi  8725  div23api  8726  div11api  8727  sup3exmid  8913  1mhlfehlf  9136  halfpm6th  9138  3halfnz  9349  addex  9650  mulex  9651  unirnioo  9972  nnenom  10433  inftonninf  10440  m1expcl2  10541  i4  10622  expnass  10625  bcn1  10737  hashinfom  10757  abs3difi  11164  0.999...  11528  ef01bndlem  11763  cos1bnd  11766  cos2bnd  11767  sin4lt0  11773  3dvdsdec  11869  3dvds2dec  11870  ndvdsi  11937  flodddiv4  11938  3lcm2e6woprm  12085  6lcm4e12  12086  3prm  12127  znnen  12398  ennnfonelem1  12407  prminf  12455  topnfn  12692  fnmgp  13130  zring0  13460  xmetunirn  13828  tgioo  14016  tgqioo  14017  addcncntoplem  14021  expcncf  14062  dveflem  14157  dvef  14158  efcn  14159  sinhalfpilem  14182  sincosq1lem  14216  sincosq4sgn  14220  cosq23lt0  14224  coseq00topi  14226  coseq0negpitopi  14227  tangtx  14229  sincos4thpi  14231  sincos6thpi  14233  pigt3  14235  cos02pilt1  14242  cos0pilt1  14243  2logb9irr  14359  2logb3irr  14361  2logb9irrALT  14362  sqrt2cxp2logb9e3  14363  2irrexpq  14364  2logb9irrap  14365  2irrexpqap  14366  lgseisenlem1  14420  lgseisenlem2  14421  ex-fl  14447  ex-exp  14449  trilpolemeq1  14758