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  2820  raltp  3680  rextp  3681  ordtriexmidlem  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  ordsoexmid  4599  funopg  5293  ftp  5750  caovass  6088  caovdi  6107  mptexw  6179  ofmres  6202  mpofvexi  6273  mpoexw  6280  dmtpos  6323  rntpos  6324  dftpos3  6329  tpostpos  6331  mapsnen  6879  xpcomen  6895  mapxpen  6918  xpmapenlem  6919  unfiexmid  6988  1lt2pi  7426  1lt2nq  7492  halfnqq  7496  m1p1sr  7846  m1m1sr  7847  suplocsrlempr  7893  addassi  8053  mulassi  8054  adddii  8055  adddiri  8056  lttri  8150  lelttri  8151  ltletri  8152  letri  8153  mul12i  8191  mul32i  8192  add12i  8208  add32i  8209  addcani  8227  addcan2i  8228  subaddi  8332  subadd2i  8333  subsub23i  8335  addsubassi  8336  addsubi  8337  subcani  8338  subcan2i  8339  pnncani  8340  subdii  8452  subdiri  8453  ltadd2i  8466  ltadd1i  8548  leadd1i  8549  leadd2i  8550  ltsubaddi  8551  lesubaddi  8552  ltsubadd2i  8553  lesubadd2i  8554  ltaddsubi  8555  gtapii  8680  mulcanapi  8713  divclapi  8800  divcanap2i  8801  divcanap1i  8802  divrecapi  8803  divcanap3i  8804  divcanap4i  8805  divassapi  8814  divdirapi  8815  div23api  8816  div11api  8817  sup3exmid  9003  1mhlfehlf  9228  halfpm6th  9230  3halfnz  9442  addex  9745  mulex  9746  unirnioo  10067  nnenom  10545  inftonninf  10553  m1expcl2  10672  i4  10753  expnass  10756  bcn1  10869  hashinfom  10889  abs3difi  11340  0.999...  11705  ef01bndlem  11940  cos1bnd  11943  cos2bnd  11944  sin4lt0  11951  3dvdsdec  12049  3dvds2dec  12050  ndvdsi  12117  flodddiv4  12120  3lcm2e6woprm  12281  6lcm4e12  12282  3prm  12323  dec2dvds  12607  modxai  12612  gcdi  12616  numexp2x  12621  2exp5  12628  2exp11  12632  znnen  12642  ennnfonelem1  12651  prminf  12699  topnfn  12948  prdsvallem  12976  prdsval  12977  fnmgp  13556  rhmex  13791  rmodislmodlem  13984  rmodislmod  13985  cnfldstr  14192  zring0  14234  fnpsr  14299  xmetunirn  14680  tgioo  14876  tgqioo  14877  addcncntoplem  14883  expcncf  14931  dveflem  15048  dvef  15049  efcn  15090  sinhalfpilem  15113  sincosq1lem  15147  sincosq4sgn  15151  cosq23lt0  15155  coseq00topi  15157  coseq0negpitopi  15158  tangtx  15160  sincos4thpi  15162  sincos6thpi  15164  pigt3  15166  cos02pilt1  15173  cos0pilt1  15174  2logb9irr  15293  2logb3irr  15295  2logb9irrALT  15296  sqrt2cxp2logb9e3  15297  2irrexpq  15298  2logb9irrap  15299  2irrexpqap  15300  1sgm2ppw  15317  lgseisenlem1  15397  lgseisenlem2  15398  lgsquadlem1  15404  ex-fl  15457  ex-exp  15459  trilpolemeq1  15775