Theorem mp3an 1371

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  vtocl3  2857  raltp  3723  rextp  3724  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  ordsoexmid  4654  funopg  5352  ftp  5824  caovass  6166  caovdi  6185  mptexw  6258  ofmres  6281  mpofvexi  6352  mpoexw  6359  dmtpos  6402  rntpos  6403  dftpos3  6408  tpostpos  6410  mapsnen  6964  xpcomen  6986  mapxpen  7009  xpmapenlem  7010  unfiexmid  7080  1lt2pi  7527  1lt2nq  7593  halfnqq  7597  m1p1sr  7947  m1m1sr  7948  suplocsrlempr  7994  addassi  8154  mulassi  8155  adddii  8156  adddiri  8157  lttri  8251  lelttri  8252  ltletri  8253  letri  8254  mul12i  8292  mul32i  8293  add12i  8309  add32i  8310  addcani  8328  addcan2i  8329  subaddi  8433  subadd2i  8434  subsub23i  8436  addsubassi  8437  addsubi  8438  subcani  8439  subcan2i  8440  pnncani  8441  subdii  8553  subdiri  8554  ltadd2i  8567  ltadd1i  8649  leadd1i  8650  leadd2i  8651  ltsubaddi  8652  lesubaddi  8653  ltsubadd2i  8654  lesubadd2i  8655  ltaddsubi  8656  gtapii  8781  mulcanapi  8814  divclapi  8901  divcanap2i  8902  divcanap1i  8903  divrecapi  8904  divcanap3i  8905  divcanap4i  8906  divassapi  8915  divdirapi  8916  div23api  8917  div11api  8918  sup3exmid  9104  1mhlfehlf  9329  halfpm6th  9331  3halfnz  9544  addex  9847  mulex  9848  unirnioo  10169  nnenom  10656  inftonninf  10664  m1expcl2  10783  i4  10864  expnass  10867  bcn1  10980  hashinfom  11000  abs3difi  11667  0.999...  12032  ef01bndlem  12267  cos1bnd  12270  cos2bnd  12271  sin4lt0  12278  3dvdsdec  12376  3dvds2dec  12377  ndvdsi  12444  flodddiv4  12447  3lcm2e6woprm  12608  6lcm4e12  12609  3prm  12650  dec2dvds  12934  modxai  12939  gcdi  12943  numexp2x  12948  2exp5  12955  2exp11  12959  znnen  12969  ennnfonelem1  12978  prminf  13026  topnfn  13277  prdsvallem  13305  prdsval  13306  fnmgp  13885  rhmex  14121  rmodislmodlem  14314  rmodislmod  14315  cnfldstr  14522  zring0  14564  fnpsr  14631  mplvalcoe  14654  fnmpl  14657  xmetunirn  15032  tgioo  15228  tgqioo  15229  addcncntoplem  15235  expcncf  15283  dveflem  15400  dvef  15401  efcn  15442  sinhalfpilem  15465  sincosq1lem  15499  sincosq4sgn  15503  cosq23lt0  15507  coseq00topi  15509  coseq0negpitopi  15510  tangtx  15512  sincos4thpi  15514  sincos6thpi  15516  pigt3  15518  cos02pilt1  15525  cos0pilt1  15526  2logb9irr  15645  2logb3irr  15647  2logb9irrALT  15648  sqrt2cxp2logb9e3  15649  2irrexpq  15650  2logb9irrap  15651  2irrexpqap  15652  1sgm2ppw  15669  lgseisenlem1  15749  lgseisenlem2  15750  lgsquadlem1  15756  ex-fl  16089  ex-exp  16091  trilpolemeq1  16408