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  2808  raltp  3664  rextp  3665  ordtriexmidlem  4536  ordtri2or2exmidlem  4543  onsucelsucexmidlem  4546  ordsoexmid  4579  funopg  5269  ftp  5722  caovass  6058  caovdi  6077  mptexw  6139  ofmres  6162  mpofvexi  6232  mpoexw  6239  dmtpos  6282  rntpos  6283  dftpos3  6288  tpostpos  6290  mapsnen  6838  xpcomen  6854  mapxpen  6877  xpmapenlem  6878  unfiexmid  6947  1lt2pi  7370  1lt2nq  7436  halfnqq  7440  m1p1sr  7790  m1m1sr  7791  suplocsrlempr  7837  addassi  7996  mulassi  7997  adddii  7998  adddiri  7999  lttri  8093  lelttri  8094  ltletri  8095  letri  8096  mul12i  8134  mul32i  8135  add12i  8151  add32i  8152  addcani  8170  addcan2i  8171  subaddi  8275  subadd2i  8276  subsub23i  8278  addsubassi  8279  addsubi  8280  subcani  8281  subcan2i  8282  pnncani  8283  subdii  8395  subdiri  8396  ltadd2i  8408  ltadd1i  8490  leadd1i  8491  leadd2i  8492  ltsubaddi  8493  lesubaddi  8494  ltsubadd2i  8495  lesubadd2i  8496  ltaddsubi  8497  gtapii  8622  mulcanapi  8655  divclapi  8742  divcanap2i  8743  divcanap1i  8744  divrecapi  8745  divcanap3i  8746  divcanap4i  8747  divassapi  8756  divdirapi  8757  div23api  8758  div11api  8759  sup3exmid  8945  1mhlfehlf  9168  halfpm6th  9170  3halfnz  9381  addex  9683  mulex  9684  unirnioo  10005  nnenom  10467  inftonninf  10474  m1expcl2  10576  i4  10657  expnass  10660  bcn1  10773  hashinfom  10793  abs3difi  11200  0.999...  11564  ef01bndlem  11799  cos1bnd  11802  cos2bnd  11803  sin4lt0  11809  3dvdsdec  11905  3dvds2dec  11906  ndvdsi  11973  flodddiv4  11974  3lcm2e6woprm  12121  6lcm4e12  12122  3prm  12163  znnen  12452  ennnfonelem1  12461  prminf  12509  topnfn  12752  fnmgp  13293  rhmex  13524  rmodislmodlem  13683  rmodislmod  13684  zring0  13916  fnpsr  13962  xmetunirn  14335  tgioo  14523  tgqioo  14524  addcncntoplem  14528  expcncf  14569  dveflem  14664  dvef  14665  efcn  14666  sinhalfpilem  14689  sincosq1lem  14723  sincosq4sgn  14727  cosq23lt0  14731  coseq00topi  14733  coseq0negpitopi  14734  tangtx  14736  sincos4thpi  14738  sincos6thpi  14740  pigt3  14742  cos02pilt1  14749  cos0pilt1  14750  2logb9irr  14866  2logb3irr  14868  2logb9irrALT  14869  sqrt2cxp2logb9e3  14870  2irrexpq  14871  2logb9irrap  14872  2irrexpqap  14873  lgseisenlem1  14928  lgseisenlem2  14929  ex-fl  14955  ex-exp  14957  trilpolemeq1  15267