Theorem mp3an 1350

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  vtocl3  2829  raltp  3690  rextp  3691  ordtriexmidlem  4568  ordtri2or2exmidlem  4575  onsucelsucexmidlem  4578  ordsoexmid  4611  funopg  5306  ftp  5771  caovass  6109  caovdi  6128  mptexw  6200  ofmres  6223  mpofvexi  6294  mpoexw  6301  dmtpos  6344  rntpos  6345  dftpos3  6350  tpostpos  6352  mapsnen  6905  xpcomen  6924  mapxpen  6947  xpmapenlem  6948  unfiexmid  7017  1lt2pi  7455  1lt2nq  7521  halfnqq  7525  m1p1sr  7875  m1m1sr  7876  suplocsrlempr  7922  addassi  8082  mulassi  8083  adddii  8084  adddiri  8085  lttri  8179  lelttri  8180  ltletri  8181  letri  8182  mul12i  8220  mul32i  8221  add12i  8237  add32i  8238  addcani  8256  addcan2i  8257  subaddi  8361  subadd2i  8362  subsub23i  8364  addsubassi  8365  addsubi  8366  subcani  8367  subcan2i  8368  pnncani  8369  subdii  8481  subdiri  8482  ltadd2i  8495  ltadd1i  8577  leadd1i  8578  leadd2i  8579  ltsubaddi  8580  lesubaddi  8581  ltsubadd2i  8582  lesubadd2i  8583  ltaddsubi  8584  gtapii  8709  mulcanapi  8742  divclapi  8829  divcanap2i  8830  divcanap1i  8831  divrecapi  8832  divcanap3i  8833  divcanap4i  8834  divassapi  8843  divdirapi  8844  div23api  8845  div11api  8846  sup3exmid  9032  1mhlfehlf  9257  halfpm6th  9259  3halfnz  9472  addex  9775  mulex  9776  unirnioo  10097  nnenom  10581  inftonninf  10589  m1expcl2  10708  i4  10789  expnass  10792  bcn1  10905  hashinfom  10925  abs3difi  11500  0.999...  11865  ef01bndlem  12100  cos1bnd  12103  cos2bnd  12104  sin4lt0  12111  3dvdsdec  12209  3dvds2dec  12210  ndvdsi  12277  flodddiv4  12280  3lcm2e6woprm  12441  6lcm4e12  12442  3prm  12483  dec2dvds  12767  modxai  12772  gcdi  12776  numexp2x  12781  2exp5  12788  2exp11  12792  znnen  12802  ennnfonelem1  12811  prminf  12859  topnfn  13109  prdsvallem  13137  prdsval  13138  fnmgp  13717  rhmex  13952  rmodislmodlem  14145  rmodislmod  14146  cnfldstr  14353  zring0  14395  fnpsr  14462  mplvalcoe  14485  fnmpl  14488  xmetunirn  14863  tgioo  15059  tgqioo  15060  addcncntoplem  15066  expcncf  15114  dveflem  15231  dvef  15232  efcn  15273  sinhalfpilem  15296  sincosq1lem  15330  sincosq4sgn  15334  cosq23lt0  15338  coseq00topi  15340  coseq0negpitopi  15341  tangtx  15343  sincos4thpi  15345  sincos6thpi  15347  pigt3  15349  cos02pilt1  15356  cos0pilt1  15357  2logb9irr  15476  2logb3irr  15478  2logb9irrALT  15479  sqrt2cxp2logb9e3  15480  2irrexpq  15481  2logb9irrap  15482  2irrexpqap  15483  1sgm2ppw  15500  lgseisenlem1  15580  lgseisenlem2  15581  lgsquadlem1  15587  ex-fl  15698  ex-exp  15700  trilpolemeq1  16016