Theorem mp3an23 1449

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 1446	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 689	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  sbciegf  3811  predeq1  6152  wrecseq1  7952  ac6sfi  8764  unfilem1  8784  ordtypelem2  8985  infxpenc2  9450  dju0en  9603  cfsmolem  9694  axdc4lem  9879  1nqenq  10386  mul02lem1  10818  muleqadd  11286  halfcl  11865  rehalfcl  11866  half0  11867  2halves  11868  halfpos2  11869  halfnneg2  11871  halfaddsub  11873  nneo  12069  zeo  12071  peano5uzi  12074  fztp  12966  uzrdgxfr  13338  bcn2  13682  bcpasc  13684  hashxplem  13797  hashfun  13801  swrds2  14304  repsw2  14314  repsw3  14315  imre  14469  reim  14470  crim  14476  addcj  14509  imval2  14512  cnpart  14601  sqrlem7  14610  absmax  14691  binomfallfaclem2  15396  bpoly2  15413  bpoly3  15414  fsumcube  15416  efgt0  15458  sinf  15479  efi4p  15492  resin4p  15493  recos4p  15494  sinneg  15501  efival  15507  cosadd  15520  sinmul  15527  sinbnd  15535  cosbnd  15536  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  sin01gt0  15545  cos01gt0  15546  sin02gt0  15547  rpnnen2lem11  15579  rpnnen2lem12  15580  odd2np1lem  15691  odd2np1  15692  pythagtriplem12  16165  pythagtriplem14  16167  pythagtriplem15  16168  pythagtriplem16  16169  pythagtriplem17  16170  pockthi  16245  prmreclem5  16258  prmreclem6  16259  prmlem0  16441  prdsplusg  16733  prdsmulr  16734  prdsvsca  16735  odinf  18692  lbsexg  19938  psgnghm2  20727  mopnex  23131  tngnm  23262  tngngp2  23263  tngngpd  23264  tngngp  23265  addccncf  23526  iihalf1  23537  iihalf2  23539  pjthlem1  24042  ovolunlem1a  24099  ovolunlem1  24100  opnmbllem  24204  vitalilem4  24214  iblcnlem1  24390  itgcnlem  24392  dvmptre  24568  dvmptim  24569  dvlipcn  24593  mdegldg  24662  aaliou3lem3  24935  aaliou3lem8  24936  sincosq1lem  25085  sincosq2sgn  25087  sincosq3sgn  25088  sincosq4sgn  25089  sinq12gt0  25095  abssinper  25108  coskpi  25110  sineq0  25111  coseq1  25112  efeq1  25115  resinf1o  25122  efif1olem2  25129  efif1olem4  25131  logneg2  25200  cxpsqrtlem  25287  cxpsqrt  25288  logsqrt  25289  1cubr  25422  leibpilem2  25521  basellem3  25662  ppiub  25782  chtublem  25789  chtub  25790  bcmax  25856  bcp1ctr  25857  bposlem2  25863  bposlem6  25867  bposlem9  25870  logdivsum  26111  4ipval2  28487  ipidsq  28489  dipcl  28491  dipcj  28493  ipasslem11  28619  hvmul0  28803  pjhthlem1  29170  h1de2bi  29333  spanunsni  29358  adjeu  29668  nmopge0  29690  nmfnge0  29706  opsqrlem6  29924  mdsl1i  30100  mdsl2bi  30102  mdexchi  30114  superpos  30133  atabsi  30180  dmdbr5ati  30201  cdj3lem1  30213  fpwrelmapffslem  30470  dp2cl  30558  dpfrac1  30570  cshw1s2  30636  ogrpaddlt  30720  ofldlt1  30888  ofldchr  30889  oddpwdc  31614  eulerpartgbij  31632  subfacp1lem2a  32429  subfacp1lem5  32433  subfacp1lem6  32434  subfaclim  32437  sinccvglem  32917  dfon2lem3  33032  dfon2lem7  33036  wsuceq1  33104  clsun  33678  vtoclefex  34617  finxpreclem5  34678  sin2h  34884  cos2h  34885  tan2h  34886  poimirlem22  34916  poimirlem31  34925  opnmbllem0  34930  mblfinlem3  34933  itg2addnclem3  34947  ftc1cnnclem  34967  ftc1anclem6  34974  ftc2nc  34978  dvasin  34980  fdc  35022  constcncf  35039  sub1cncf  35041  sub2cncf  35042  heiborlem7  35097  atlatmstc  36457  fac2xp3  39101  facp2  39102  sn-00idlem1  39235  0prjspnlem  39275  diophren  39417  dftrcl3  40072  dfrtrcl3  40085  cotrclrcl  40094  lhe4.4ex1a  40668  dirkerper  42388  zlmodzxznm  44559  sinh-conventional  44845