Theorem mp3an 1378

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  vtocl3  2879  raltp  3762  rextp  3763  ordtriexmidlem  4661  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  ordsoexmid  4704  funopg  5406  ftp  5891  caovass  6240  caovdi  6259  mptexw  6332  ofmres  6359  mpofvexi  6432  mpoexw  6439  dmtpos  6517  rntpos  6518  dftpos3  6523  tpostpos  6525  mapsnen  7090  xpcomen  7115  mapxpen  7138  xpmapenlem  7139  unfiexmid  7215  1lt2pi  7697  1lt2nq  7763  halfnqq  7767  m1p1sr  8117  m1m1sr  8118  suplocsrlempr  8164  addassi  8324  mulassi  8325  adddii  8326  adddiri  8327  lttri  8420  lelttri  8421  ltletri  8422  letri  8423  mul12i  8462  mul32i  8463  add12i  8479  add32i  8480  addcani  8498  addcan2i  8499  subaddi  8603  subadd2i  8604  subsub23i  8606  addsubassi  8607  addsubi  8608  subcani  8609  subcan2i  8610  pnncani  8611  subdii  8724  subdiri  8725  ltadd2i  8738  ltadd1i  8820  leadd1i  8821  leadd2i  8822  ltsubaddi  8823  lesubaddi  8824  ltsubadd2i  8825  lesubadd2i  8826  ltaddsubi  8827  gtapii  8952  mulcanapi  8985  divclapi  9074  divcanap2i  9075  divcanap1i  9076  divrecapi  9077  divcanap3i  9078  divcanap4i  9079  divassapi  9088  divdirapi  9089  div23api  9090  div11api  9091  sup3exmid  9277  1mhlfehlf  9502  halfpm6th  9504  3halfnz  9722  addex  10031  mulex  10032  unirnioo  10354  nnenom  10849  inftonninf  10857  m1expcl2  10976  i4  11057  expnass  11060  bcn1  11174  hashinfom  11195  abs3difi  11900  0.999...  12266  ef01bndlem  12501  cos1bnd  12504  cos2bnd  12505  sin4lt0  12512  3dvdsdec  12610  3dvds2dec  12611  ndvdsi  12678  flodddiv4  12681  3lcm2e6woprm  12842  6lcm4e12  12843  3prm  12884  dec2dvds  13168  modxai  13173  gcdi  13177  numexp2x  13182  2exp5  13189  2exp11  13193  ballotfilem2  13206  ballotfilemafi  13216  ballotfilembfi  13217  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemth  13259  znnen  13267  ennnfonelem1  13276  prminf  13324  topnfn  13575  prdsvallem  13598  prdsval  14150  fnmgp  14196  rhmex  14437  rmodislmodlem  14659  rmodislmod  14660  cnfldstr  14867  zring0  14907  fnpsr  14974  mplvalcoe  15004  fnmpl  15007  xmetunirn  15382  tgioo  15578  tgqioo  15579  addcncntoplem  15585  expcncf  15633  dveflem  15750  dvef  15751  efcn  15792  sinhalfpilem  15815  sincosq1lem  15849  sincosq4sgn  15853  cosq23lt0  15857  coseq00topi  15859  coseq0negpitopi  15860  tangtx  15862  sincos4thpi  15864  sincos6thpi  15866  pigt3  15868  cos02pilt1  15875  cos0pilt1  15876  2logb9irr  15996  2logb3irr  15998  2logb9irrALT  15999  sqrt2cxp2logb9e3  16000  2irrexpq  16001  2logb9irrap  16002  2irrexpqap  16003  1sgm2ppw  16023  lgseisenlem1  16103  lgseisenlem2  16104  lgsquadlem1  16110  upgr2wlkdc  16532  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  ex-fl  16653  ex-exp  16655  repiecelem  16979  repiecege0  16981  trilpolemeq1  16994