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  2861  raltp  3730  rextp  3731  ordtriexmidlem  4623  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  ordsoexmid  4666  funopg  5367  ftp  5847  caovass  6193  caovdi  6212  mptexw  6284  ofmres  6307  mpofvexi  6380  mpoexw  6387  dmtpos  6465  rntpos  6466  dftpos3  6471  tpostpos  6473  mapsnen  7029  xpcomen  7054  mapxpen  7077  xpmapenlem  7078  unfiexmid  7153  1lt2pi  7620  1lt2nq  7686  halfnqq  7690  m1p1sr  8040  m1m1sr  8041  suplocsrlempr  8087  addassi  8247  mulassi  8248  adddii  8249  adddiri  8250  lttri  8343  lelttri  8344  ltletri  8345  letri  8346  mul12i  8384  mul32i  8385  add12i  8401  add32i  8402  addcani  8420  addcan2i  8421  subaddi  8525  subadd2i  8526  subsub23i  8528  addsubassi  8529  addsubi  8530  subcani  8531  subcan2i  8532  pnncani  8533  subdii  8645  subdiri  8646  ltadd2i  8659  ltadd1i  8741  leadd1i  8742  leadd2i  8743  ltsubaddi  8744  lesubaddi  8745  ltsubadd2i  8746  lesubadd2i  8747  ltaddsubi  8748  gtapii  8873  mulcanapi  8906  divclapi  8993  divcanap2i  8994  divcanap1i  8995  divrecapi  8996  divcanap3i  8997  divcanap4i  8998  divassapi  9007  divdirapi  9008  div23api  9009  div11api  9010  sup3exmid  9196  1mhlfehlf  9421  halfpm6th  9423  3halfnz  9638  addex  9947  mulex  9948  unirnioo  10269  nnenom  10759  inftonninf  10767  m1expcl2  10886  i4  10967  expnass  10970  bcn1  11083  hashinfom  11103  abs3difi  11796  0.999...  12162  ef01bndlem  12397  cos1bnd  12400  cos2bnd  12401  sin4lt0  12408  3dvdsdec  12506  3dvds2dec  12507  ndvdsi  12574  flodddiv4  12577  3lcm2e6woprm  12738  6lcm4e12  12739  3prm  12780  dec2dvds  13064  modxai  13069  gcdi  13073  numexp2x  13078  2exp5  13085  2exp11  13089  znnen  13099  ennnfonelem1  13108  prminf  13156  topnfn  13407  prdsvallem  13435  prdsval  13436  fnmgp  14016  rhmex  14252  rmodislmodlem  14446  rmodislmod  14447  cnfldstr  14654  zring0  14696  fnpsr  14763  mplvalcoe  14791  fnmpl  14794  xmetunirn  15169  tgioo  15365  tgqioo  15366  addcncntoplem  15372  expcncf  15420  dveflem  15537  dvef  15538  efcn  15579  sinhalfpilem  15602  sincosq1lem  15636  sincosq4sgn  15640  cosq23lt0  15644  coseq00topi  15646  coseq0negpitopi  15647  tangtx  15649  sincos4thpi  15651  sincos6thpi  15653  pigt3  15655  cos02pilt1  15662  cos0pilt1  15663  2logb9irr  15782  2logb3irr  15784  2logb9irrALT  15785  sqrt2cxp2logb9e3  15786  2irrexpq  15787  2logb9irrap  15788  2irrexpqap  15789  1sgm2ppw  15809  lgseisenlem1  15889  lgseisenlem2  15890  lgsquadlem1  15896  upgr2wlkdc  16318  konigsberglem1  16429  konigsberglem2  16430  konigsberglem3  16431  konigsberglem5  16433  ex-fl  16439  ex-exp  16441  repiecelem  16757  repiecege0  16759  trilpolemeq1  16772