Theorem mp3an 1348

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  vtocl3  2820  raltp  3680  rextp  3681  ordtriexmidlem  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsoexmid  4599  funopg  5293  ftp  5750  caovass  6088  caovdi  6107  mptexw  6179  ofmres  6202  mpofvexi  6273  mpoexw  6280  dmtpos  6323  rntpos  6324  dftpos3  6329  tpostpos  6331  mapsnen  6879  xpcomen  6895  mapxpen  6918  xpmapenlem  6919  unfiexmid  6988  1lt2pi  7424  1lt2nq  7490  halfnqq  7494  m1p1sr  7844  m1m1sr  7845  suplocsrlempr  7891  addassi  8051  mulassi  8052  adddii  8053  adddiri  8054  lttri  8148  lelttri  8149  ltletri  8150  letri  8151  mul12i  8189  mul32i  8190  add12i  8206  add32i  8207  addcani  8225  addcan2i  8226  subaddi  8330  subadd2i  8331  subsub23i  8333  addsubassi  8334  addsubi  8335  subcani  8336  subcan2i  8337  pnncani  8338  subdii  8450  subdiri  8451  ltadd2i  8464  ltadd1i  8546  leadd1i  8547  leadd2i  8548  ltsubaddi  8549  lesubaddi  8550  ltsubadd2i  8551  lesubadd2i  8552  ltaddsubi  8553  gtapii  8678  mulcanapi  8711  divclapi  8798  divcanap2i  8799  divcanap1i  8800  divrecapi  8801  divcanap3i  8802  divcanap4i  8803  divassapi  8812  divdirapi  8813  div23api  8814  div11api  8815  sup3exmid  9001  1mhlfehlf  9226  halfpm6th  9228  3halfnz  9440  addex  9743  mulex  9744  unirnioo  10065  nnenom  10543  inftonninf  10551  m1expcl2  10670  i4  10751  expnass  10754  bcn1  10867  hashinfom  10887  abs3difi  11338  0.999...  11703  ef01bndlem  11938  cos1bnd  11941  cos2bnd  11942  sin4lt0  11949  3dvdsdec  12047  3dvds2dec  12048  ndvdsi  12115  flodddiv4  12118  3lcm2e6woprm  12279  6lcm4e12  12280  3prm  12321  dec2dvds  12605  modxai  12610  gcdi  12614  numexp2x  12619  2exp5  12626  2exp11  12630  znnen  12640  ennnfonelem1  12649  prminf  12697  topnfn  12946  prdsvallem  12974  prdsval  12975  fnmgp  13554  rhmex  13789  rmodislmodlem  13982  rmodislmod  13983  cnfldstr  14190  zring0  14232  fnpsr  14297  xmetunirn  14678  tgioo  14874  tgqioo  14875  addcncntoplem  14881  expcncf  14929  dveflem  15046  dvef  15047  efcn  15088  sinhalfpilem  15111  sincosq1lem  15145  sincosq4sgn  15149  cosq23lt0  15153  coseq00topi  15155  coseq0negpitopi  15156  tangtx  15158  sincos4thpi  15160  sincos6thpi  15162  pigt3  15164  cos02pilt1  15171  cos0pilt1  15172  2logb9irr  15291  2logb3irr  15293  2logb9irrALT  15294  sqrt2cxp2logb9e3  15295  2irrexpq  15296  2logb9irrap  15297  2irrexpqap  15298  1sgm2ppw  15315  lgseisenlem1  15395  lgseisenlem2  15396  lgsquadlem1  15402  ex-fl  15455  ex-exp  15457  trilpolemeq1  15771