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  5838  caovass  6182  caovdi  6201  mptexw  6274  ofmres  6297  mpofvexi  6370  mpoexw  6377  dmtpos  6421  rntpos  6422  dftpos3  6427  tpostpos  6429  mapsnen  6985  xpcomen  7010  mapxpen  7033  xpmapenlem  7034  unfiexmid  7109  1lt2pi  7559  1lt2nq  7625  halfnqq  7629  m1p1sr  7979  m1m1sr  7980  suplocsrlempr  8026  addassi  8186  mulassi  8187  adddii  8188  adddiri  8189  lttri  8283  lelttri  8284  ltletri  8285  letri  8286  mul12i  8324  mul32i  8325  add12i  8341  add32i  8342  addcani  8360  addcan2i  8361  subaddi  8465  subadd2i  8466  subsub23i  8468  addsubassi  8469  addsubi  8470  subcani  8471  subcan2i  8472  pnncani  8473  subdii  8585  subdiri  8586  ltadd2i  8599  ltadd1i  8681  leadd1i  8682  leadd2i  8683  ltsubaddi  8684  lesubaddi  8685  ltsubadd2i  8686  lesubadd2i  8687  ltaddsubi  8688  gtapii  8813  mulcanapi  8846  divclapi  8933  divcanap2i  8934  divcanap1i  8935  divrecapi  8936  divcanap3i  8937  divcanap4i  8938  divassapi  8947  divdirapi  8948  div23api  8949  div11api  8950  sup3exmid  9136  1mhlfehlf  9361  halfpm6th  9363  3halfnz  9576  addex  9885  mulex  9886  unirnioo  10207  nnenom  10695  inftonninf  10703  m1expcl2  10822  i4  10903  expnass  10906  bcn1  11019  hashinfom  11039  abs3difi  11716  0.999...  12081  ef01bndlem  12316  cos1bnd  12319  cos2bnd  12320  sin4lt0  12327  3dvdsdec  12425  3dvds2dec  12426  ndvdsi  12493  flodddiv4  12496  3lcm2e6woprm  12657  6lcm4e12  12658  3prm  12699  dec2dvds  12983  modxai  12988  gcdi  12992  numexp2x  12997  2exp5  13004  2exp11  13008  znnen  13018  ennnfonelem1  13027  prminf  13075  topnfn  13326  prdsvallem  13354  prdsval  13355  fnmgp  13934  rhmex  14170  rmodislmodlem  14363  rmodislmod  14364  cnfldstr  14571  zring0  14613  fnpsr  14680  mplvalcoe  14703  fnmpl  14706  xmetunirn  15081  tgioo  15277  tgqioo  15278  addcncntoplem  15284  expcncf  15332  dveflem  15449  dvef  15450  efcn  15491  sinhalfpilem  15514  sincosq1lem  15548  sincosq4sgn  15552  cosq23lt0  15556  coseq00topi  15558  coseq0negpitopi  15559  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  pigt3  15567  cos02pilt1  15574  cos0pilt1  15575  2logb9irr  15694  2logb3irr  15696  2logb9irrALT  15697  sqrt2cxp2logb9e3  15698  2irrexpq  15699  2logb9irrap  15700  2irrexpqap  15701  1sgm2ppw  15718  lgseisenlem1  15798  lgseisenlem2  15799  lgsquadlem1  15805  upgr2wlkdc  16227  ex-fl  16321  ex-exp  16323  trilpolemeq1  16644