Theorem mp3an 1315

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

Syntax hints:   → wi 4   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  vtocl3  2742  raltp  3580  rextp  3581  ordtriexmidlem  4435  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  ordsoexmid  4477  funopg  5157  ftp  5605  caovass  5931  caovdi  5950  ofmres  6034  mpofvexi  6104  dmtpos  6153  rntpos  6154  dftpos3  6159  tpostpos  6161  mapsnen  6705  xpcomen  6721  mapxpen  6742  xpmapenlem  6743  unfiexmid  6806  1lt2pi  7148  1lt2nq  7214  halfnqq  7218  m1p1sr  7568  m1m1sr  7569  suplocsrlempr  7615  addassi  7774  mulassi  7775  adddii  7776  adddiri  7777  lttri  7868  lelttri  7869  ltletri  7870  letri  7871  mul12i  7908  mul32i  7909  add12i  7925  add32i  7926  addcani  7944  addcan2i  7945  subaddi  8049  subadd2i  8050  subsub23i  8052  addsubassi  8053  addsubi  8054  subcani  8055  subcan2i  8056  pnncani  8057  subdii  8169  subdiri  8170  ltadd2i  8182  ltadd1i  8264  leadd1i  8265  leadd2i  8266  ltsubaddi  8267  lesubaddi  8268  ltsubadd2i  8269  lesubadd2i  8270  ltaddsubi  8271  gtapii  8396  mulcanapi  8428  divclapi  8514  divcanap2i  8515  divcanap1i  8516  divrecapi  8517  divcanap3i  8518  divcanap4i  8519  divassapi  8528  divdirapi  8529  div23api  8530  div11api  8531  sup3exmid  8715  1mhlfehlf  8938  halfpm6th  8940  3halfnz  9148  unirnioo  9756  nnenom  10207  inftonninf  10214  m1expcl2  10315  i4  10395  expnass  10398  bcn1  10504  hashinfom  10524  abs3difi  10928  0.999...  11290  ef01bndlem  11463  cos1bnd  11466  cos2bnd  11467  sin4lt0  11473  3dvdsdec  11562  3dvds2dec  11563  ndvdsi  11630  flodddiv4  11631  3lcm2e6woprm  11767  6lcm4e12  11768  3prm  11809  znnen  11911  ennnfonelem1  11920  topnfn  12125  xmetunirn  12527  tgioo  12715  tgqioo  12716  addcncntoplem  12720  expcncf  12761  dveflem  12855  dvef  12856  efcn  12857  sinhalfpilem  12872  sincosq1lem  12906  sincosq4sgn  12910  cosq23lt0  12914  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  sincos4thpi  12921  sincos6thpi  12923  pigt3  12925  cos02pilt1  12932  ex-fl  12937  ex-exp  12939  trilpolemeq1  13233