Theorem mp3an 1374

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  vtocl3  2871  raltp  3746  rextp  3747  ordtriexmidlem  4641  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  ordsoexmid  4684  funopg  5386  ftp  5869  caovass  6215  caovdi  6234  mptexw  6306  ofmres  6329  mpofvexi  6402  mpoexw  6409  dmtpos  6487  rntpos  6488  dftpos3  6493  tpostpos  6495  mapsnen  7053  xpcomen  7078  mapxpen  7101  xpmapenlem  7102  unfiexmid  7178  1lt2pi  7655  1lt2nq  7721  halfnqq  7725  m1p1sr  8075  m1m1sr  8076  suplocsrlempr  8122  addassi  8282  mulassi  8283  adddii  8284  adddiri  8285  lttri  8378  lelttri  8379  ltletri  8380  letri  8381  mul12i  8419  mul32i  8420  add12i  8436  add32i  8437  addcani  8455  addcan2i  8456  subaddi  8560  subadd2i  8561  subsub23i  8563  addsubassi  8564  addsubi  8565  subcani  8566  subcan2i  8567  pnncani  8568  subdii  8680  subdiri  8681  ltadd2i  8694  ltadd1i  8776  leadd1i  8777  leadd2i  8778  ltsubaddi  8779  lesubaddi  8780  ltsubadd2i  8781  lesubadd2i  8782  ltaddsubi  8783  gtapii  8908  mulcanapi  8941  divclapi  9028  divcanap2i  9029  divcanap1i  9030  divrecapi  9031  divcanap3i  9032  divcanap4i  9033  divassapi  9042  divdirapi  9043  div23api  9044  div11api  9045  sup3exmid  9231  1mhlfehlf  9456  halfpm6th  9458  3halfnz  9675  addex  9984  mulex  9985  unirnioo  10306  nnenom  10796  inftonninf  10804  m1expcl2  10923  i4  11004  expnass  11007  bcn1  11120  hashinfom  11141  abs3difi  11841  0.999...  12207  ef01bndlem  12442  cos1bnd  12445  cos2bnd  12446  sin4lt0  12453  3dvdsdec  12551  3dvds2dec  12552  ndvdsi  12619  flodddiv4  12622  3lcm2e6woprm  12783  6lcm4e12  12784  3prm  12825  dec2dvds  13109  modxai  13114  gcdi  13118  numexp2x  13123  2exp5  13130  2exp11  13134  ballotfilem2  13142  znnen  13149  ennnfonelem1  13158  prminf  13206  topnfn  13457  prdsvallem  13485  prdsval  13486  fnmgp  14066  rhmex  14302  rmodislmodlem  14498  rmodislmod  14499  cnfldstr  14706  zring0  14748  fnpsr  14815  mplvalcoe  14845  fnmpl  14848  xmetunirn  15223  tgioo  15419  tgqioo  15420  addcncntoplem  15426  expcncf  15474  dveflem  15591  dvef  15592  efcn  15633  sinhalfpilem  15656  sincosq1lem  15690  sincosq4sgn  15694  cosq23lt0  15698  coseq00topi  15700  coseq0negpitopi  15701  tangtx  15703  sincos4thpi  15705  sincos6thpi  15707  pigt3  15709  cos02pilt1  15716  cos0pilt1  15717  2logb9irr  15836  2logb3irr  15838  2logb9irrALT  15839  sqrt2cxp2logb9e3  15840  2irrexpq  15841  2logb9irrap  15842  2irrexpqap  15843  1sgm2ppw  15863  lgseisenlem1  15943  lgseisenlem2  15944  lgsquadlem1  15950  upgr2wlkdc  16372  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  ex-fl  16493  ex-exp  16495  repiecelem  16809  repiecege0  16811  trilpolemeq1  16824