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  2737  raltp  3575  rextp  3576  ordtriexmidlem  4430  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  ordsoexmid  4472  funopg  5152  ftp  5598  caovass  5924  caovdi  5943  ofmres  6027  mpofvexi  6097  dmtpos  6146  rntpos  6147  dftpos3  6152  tpostpos  6154  mapsnen  6698  xpcomen  6714  mapxpen  6735  xpmapenlem  6736  unfiexmid  6799  1lt2pi  7141  1lt2nq  7207  halfnqq  7211  m1p1sr  7561  m1m1sr  7562  suplocsrlempr  7608  addassi  7767  mulassi  7768  adddii  7769  adddiri  7770  lttri  7861  lelttri  7862  ltletri  7863  letri  7864  mul12i  7901  mul32i  7902  add12i  7918  add32i  7919  addcani  7937  addcan2i  7938  subaddi  8042  subadd2i  8043  subsub23i  8045  addsubassi  8046  addsubi  8047  subcani  8048  subcan2i  8049  pnncani  8050  subdii  8162  subdiri  8163  ltadd2i  8175  ltadd1i  8257  leadd1i  8258  leadd2i  8259  ltsubaddi  8260  lesubaddi  8261  ltsubadd2i  8262  lesubadd2i  8263  ltaddsubi  8264  gtapii  8389  mulcanapi  8421  divclapi  8507  divcanap2i  8508  divcanap1i  8509  divrecapi  8510  divcanap3i  8511  divcanap4i  8512  divassapi  8521  divdirapi  8522  div23api  8523  div11api  8524  sup3exmid  8708  1mhlfehlf  8931  halfpm6th  8933  3halfnz  9141  unirnioo  9749  nnenom  10200  inftonninf  10207  m1expcl2  10308  i4  10388  expnass  10391  bcn1  10497  hashinfom  10517  abs3difi  10921  0.999...  11283  ef01bndlem  11452  cos1bnd  11455  cos2bnd  11456  sin4lt0  11462  3dvdsdec  11551  3dvds2dec  11552  ndvdsi  11619  flodddiv4  11620  3lcm2e6woprm  11756  6lcm4e12  11757  3prm  11798  znnen  11900  ennnfonelem1  11909  topnfn  12114  xmetunirn  12516  tgioo  12704  tgqioo  12705  addcncntoplem  12709  expcncf  12750  dveflem  12844  dvef  12845  efcn  12846  sinhalfpilem  12861  sincosq1lem  12895  sincosq4sgn  12899  cosq23lt0  12903  coseq00topi  12905  coseq0negpitopi  12906  tangtx  12908  sincos4thpi  12910  sincos6thpi  12912  pigt3  12914  cos02pilt1  12921  ex-fl  12926  ex-exp  12928  trilpolemeq1  13222