Theorem mp3an 1373

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  vtocl3  2860  raltp  3726  rextp  3727  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  ordsoexmid  4660  funopg  5360  ftp  5839  caovass  6183  caovdi  6202  mptexw  6275  ofmres  6298  mpofvexi  6371  mpoexw  6378  dmtpos  6422  rntpos  6423  dftpos3  6428  tpostpos  6430  mapsnen  6986  xpcomen  7011  mapxpen  7034  xpmapenlem  7035  unfiexmid  7110  1lt2pi  7560  1lt2nq  7626  halfnqq  7630  m1p1sr  7980  m1m1sr  7981  suplocsrlempr  8027  addassi  8187  mulassi  8188  adddii  8189  adddiri  8190  lttri  8284  lelttri  8285  ltletri  8286  letri  8287  mul12i  8325  mul32i  8326  add12i  8342  add32i  8343  addcani  8361  addcan2i  8362  subaddi  8466  subadd2i  8467  subsub23i  8469  addsubassi  8470  addsubi  8471  subcani  8472  subcan2i  8473  pnncani  8474  subdii  8586  subdiri  8587  ltadd2i  8600  ltadd1i  8682  leadd1i  8683  leadd2i  8684  ltsubaddi  8685  lesubaddi  8686  ltsubadd2i  8687  lesubadd2i  8688  ltaddsubi  8689  gtapii  8814  mulcanapi  8847  divclapi  8934  divcanap2i  8935  divcanap1i  8936  divrecapi  8937  divcanap3i  8938  divcanap4i  8939  divassapi  8948  divdirapi  8949  div23api  8950  div11api  8951  sup3exmid  9137  1mhlfehlf  9362  halfpm6th  9364  3halfnz  9577  addex  9886  mulex  9887  unirnioo  10208  nnenom  10697  inftonninf  10705  m1expcl2  10824  i4  10905  expnass  10908  bcn1  11021  hashinfom  11041  abs3difi  11734  0.999...  12100  ef01bndlem  12335  cos1bnd  12338  cos2bnd  12339  sin4lt0  12346  3dvdsdec  12444  3dvds2dec  12445  ndvdsi  12512  flodddiv4  12515  3lcm2e6woprm  12676  6lcm4e12  12677  3prm  12718  dec2dvds  13002  modxai  13007  gcdi  13011  numexp2x  13016  2exp5  13023  2exp11  13027  znnen  13037  ennnfonelem1  13046  prminf  13094  topnfn  13345  prdsvallem  13373  prdsval  13374  fnmgp  13954  rhmex  14190  rmodislmodlem  14383  rmodislmod  14384  cnfldstr  14591  zring0  14633  fnpsr  14700  mplvalcoe  14723  fnmpl  14726  xmetunirn  15101  tgioo  15297  tgqioo  15298  addcncntoplem  15304  expcncf  15352  dveflem  15469  dvef  15470  efcn  15511  sinhalfpilem  15534  sincosq1lem  15568  sincosq4sgn  15572  cosq23lt0  15576  coseq00topi  15578  coseq0negpitopi  15579  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  pigt3  15587  cos02pilt1  15594  cos0pilt1  15595  2logb9irr  15714  2logb3irr  15716  2logb9irrALT  15717  sqrt2cxp2logb9e3  15718  2irrexpq  15719  2logb9irrap  15720  2irrexpqap  15721  1sgm2ppw  15738  lgseisenlem1  15818  lgseisenlem2  15819  lgsquadlem1  15825  upgr2wlkdc  16247  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem5  16362  ex-fl  16368  ex-exp  16370  trilpolemeq1  16695