Theorem mp3an 1348

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  vtocl3  2816  raltp  3675  rextp  3676  ordtriexmidlem  4551  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  ordsoexmid  4594  funopg  5288  ftp  5743  caovass  6079  caovdi  6098  mptexw  6165  ofmres  6188  mpofvexi  6259  mpoexw  6266  dmtpos  6309  rntpos  6310  dftpos3  6315  tpostpos  6317  mapsnen  6865  xpcomen  6881  mapxpen  6904  xpmapenlem  6905  unfiexmid  6974  1lt2pi  7400  1lt2nq  7466  halfnqq  7470  m1p1sr  7820  m1m1sr  7821  suplocsrlempr  7867  addassi  8027  mulassi  8028  adddii  8029  adddiri  8030  lttri  8124  lelttri  8125  ltletri  8126  letri  8127  mul12i  8165  mul32i  8166  add12i  8182  add32i  8183  addcani  8201  addcan2i  8202  subaddi  8306  subadd2i  8307  subsub23i  8309  addsubassi  8310  addsubi  8311  subcani  8312  subcan2i  8313  pnncani  8314  subdii  8426  subdiri  8427  ltadd2i  8439  ltadd1i  8521  leadd1i  8522  leadd2i  8523  ltsubaddi  8524  lesubaddi  8525  ltsubadd2i  8526  lesubadd2i  8527  ltaddsubi  8528  gtapii  8653  mulcanapi  8686  divclapi  8773  divcanap2i  8774  divcanap1i  8775  divrecapi  8776  divcanap3i  8777  divcanap4i  8778  divassapi  8787  divdirapi  8788  div23api  8789  div11api  8790  sup3exmid  8976  1mhlfehlf  9200  halfpm6th  9202  3halfnz  9414  addex  9717  mulex  9718  unirnioo  10039  nnenom  10505  inftonninf  10513  m1expcl2  10632  i4  10713  expnass  10716  bcn1  10829  hashinfom  10849  abs3difi  11300  0.999...  11664  ef01bndlem  11899  cos1bnd  11902  cos2bnd  11903  sin4lt0  11910  3dvdsdec  12006  3dvds2dec  12007  ndvdsi  12074  flodddiv4  12075  3lcm2e6woprm  12224  6lcm4e12  12225  3prm  12266  znnen  12555  ennnfonelem1  12564  prminf  12612  topnfn  12855  fnmgp  13418  rhmex  13653  rmodislmodlem  13846  rmodislmod  13847  zring0  14088  fnpsr  14153  xmetunirn  14526  tgioo  14714  tgqioo  14715  addcncntoplem  14719  expcncf  14763  dveflem  14872  dvef  14873  efcn  14903  sinhalfpilem  14926  sincosq1lem  14960  sincosq4sgn  14964  cosq23lt0  14968  coseq00topi  14970  coseq0negpitopi  14971  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  pigt3  14979  cos02pilt1  14986  cos0pilt1  14987  2logb9irr  15103  2logb3irr  15105  2logb9irrALT  15106  sqrt2cxp2logb9e3  15107  2irrexpq  15108  2logb9irrap  15109  2irrexpqap  15110  lgseisenlem1  15186  lgseisenlem2  15187  lgsquadlem1  15191  ex-fl  15217  ex-exp  15219  trilpolemeq1  15530