Theorem mp3an23 1456

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	⊢ 𝜓
mp3an23.2	⊢ 𝜒
mp3an23.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 ⊢ 𝜓
2		mp3an23.2	. . 3 ⊢ 𝜒
3		mp3an23.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1453	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 692	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  sbciegf  3767  predeq1  6267  wrecseq1  8265  ac6sfi  9194  unfilem1  9215  fiint  9237  ordtypelem2  9434  infxpenc2  9944  dju0en  10098  cfsmolem  10192  axdc4lem  10377  1nqenq  10885  mul02lem1  11322  muleqadd  11794  2halves  12395  halfcl  12403  rehalfcl  12404  half0  12405  halfpos2  12406  halfnneg2  12408  halfaddsub  12410  nneo  12613  zeo  12615  peano5uzi  12618  fztp  13534  uzrdgxfr  13929  bcn2  14281  bcpasc  14283  hashxplem  14395  hashfun  14399  swrds2  14902  repsw2  14912  repsw3  14913  imre  15070  reim  15071  crim  15077  addcj  15110  imval2  15113  cnpart  15202  01sqrexlem7  15210  absmax  15292  binomfallfaclem2  16005  bpoly2  16022  bpoly3  16023  fsumcube  16025  efgt0  16070  sinf  16091  efi4p  16104  resin4p  16105  recos4p  16106  sinneg  16113  efival  16119  cosadd  16132  sinmul  16139  sinbnd  16147  cosbnd  16148  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  sin01gt0  16157  cos01gt0  16158  sin02gt0  16159  rpnnen2lem11  16191  rpnnen2lem12  16192  odd2np1lem  16309  odd2np1  16310  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem16  16801  pythagtriplem17  16802  pockthi  16878  prmreclem5  16891  prmreclem6  16892  prmlem0  17076  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  isghm  19190  odinf  19538  ogrpaddlt  20113  ofldlt1  20852  lbsexg  21162  ofldchr  21556  psgnghm2  21561  mopnex  24484  tngnm  24616  tngngp2  24617  tngngpd  24618  tngngp  24619  addccncf  24884  sub1cncf  24886  sub2cncf  24887  iihalf1  24898  iihalf2  24900  pjthlem1  25404  ovolunlem1a  25463  ovolunlem1  25464  opnmbllem  25568  vitalilem4  25578  iblcnlem1  25755  itgcnlem  25757  dvmptre  25936  dvmptim  25937  dvlipcn  25961  mdegldg  26031  aaliou3lem3  26310  aaliou3lem8  26311  sincosq1lem  26461  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  sinq12gt0  26471  abssinper  26485  coskpi  26487  sineq0  26488  coseq1  26489  efeq1  26492  resinf1o  26500  efif1olem2  26507  efif1olem4  26509  logneg2  26579  cxpsqrtlem  26666  cxpsqrt  26667  logsqrt  26668  1cubr  26806  leibpilem2  26905  basellem3  27046  ppiub  27167  chtublem  27174  chtub  27175  bcmax  27241  bcp1ctr  27242  bposlem2  27248  bposlem6  27252  bposlem9  27255  logdivsum  27496  elno  27609  mulscl  28126  4ipval2  30779  ipidsq  30781  dipcl  30783  dipcj  30785  ipasslem11  30911  hvmul0  31095  pjhthlem1  31462  h1de2bi  31625  spanunsni  31650  adjeu  31960  nmopge0  31982  nmfnge0  31998  opsqrlem6  32216  mdsl1i  32392  mdsl2bi  32394  mdexchi  32406  superpos  32425  atabsi  32472  dmdbr5ati  32493  cdj3lem1  32505  fpwrelmapffslem  32805  dp2cl  32939  dpfrac1  32951  cshw1s2  33020  oddpwdc  34498  eulerpartgbij  34516  subfacp1lem2a  35362  subfacp1lem5  35366  subfacp1lem6  35367  subfaclim  35370  sinccvglem  35854  dfon2lem3  35965  dfon2lem7  35969  wsuceq1  35995  clsun  36510  vtoclefex  37650  finxpreclem5  37711  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem22  37963  poimirlem31  37972  opnmbllem0  37977  mblfinlem3  37980  itg2addnclem3  37994  ftc1cnnclem  38012  ftc1anclem6  38019  ftc2nc  38023  dvasin  38025  fdc  38066  constcncf  38083  heiborlem7  38138  atlatmstc  39765  lcmineqlem10  42477  lcmineqlem12  42479  facp2  42582  3rdpwhole  42724  sn-00idlem1  42830  0prjspnlem  43056  sn-isghm  43106  diophren  43241  oaabsb  43722  dftrcl3  44147  dfrtrcl3  44160  cotrclrcl  44169  lhe4.4ex1a  44756  dirkerper  46524  sinnpoly  47339  zlmodzxznm  48973  sinh-conventional  50214