Theorem mp3an23 1479

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  sbciegf  3789  predeq1  6305  wrecseq1  8312  ac6sfi  9244  unfilem1  9265  fiint  9286  ordtypelem2  9481  infxpenc2  10006  dju0en  10159  cfsmolem  10254  axdc4lem  10439  1nqenq  10947  mul02lem1  11386  muleqadd  11858  2halves  12462  halfcl  12470  rehalfcl  12471  half0  12472  halfpos2  12473  halfnneg2  12475  halfaddsub  12477  nneo  12680  zeo  12682  peano5uzi  12685  fztp  13608  uzrdgxfr  14003  bcn2  14355  bcpasc  14357  hashxplem  14470  hashfun  14474  swrds2  14977  repsw2  14987  repsw3  14988  imre  15159  reim  15160  crim  15166  addcj  15199  imval2  15202  cnpart  15291  01sqrexlem7  15299  absmax  15381  binomfallfaclem2  16094  bpoly2  16111  bpoly3  16112  fsumcube  16114  efgt0  16159  sinf  16180  efi4p  16193  resin4p  16194  recos4p  16195  sinneg  16202  efival  16208  cosadd  16221  sinmul  16228  sinbnd  16236  cosbnd  16237  ef01bndlem  16240  sin01bnd  16241  cos01bnd  16242  sin01gt0  16246  cos01gt0  16247  sin02gt0  16248  rpnnen2lem11  16280  rpnnen2lem12  16281  odd2np1lem  16398  odd2np1  16399  pythagtriplem12  16886  pythagtriplem14  16888  pythagtriplem15  16889  pythagtriplem16  16890  pythagtriplem17  16891  pockthi  16967  prmreclem5  16980  prmreclem6  16981  prmlem0  17165  prdsplusg  17511  prdsmulr  17512  prdsvsca  17513  isghm  19286  odinf  19633  ogrpaddlt  20208  ofldlt1  20956  lbsexg  21266  ofldchr  21695  psgnghm2  21700  mopnex  24645  tngnm  24777  tngngp2  24778  tngngpd  24779  tngngp  24780  addccncf  25045  sub1cncf  25047  sub2cncf  25048  iihalf1  25059  iihalf2  25061  pjthlem1  25565  ovolunlem1a  25624  ovolunlem1  25625  opnmbllem  25729  vitalilem4  25739  iblcnlem1  25916  itgcnlem  25918  dvmptre  26097  dvmptim  26098  dvlipcn  26122  mdegldg  26192  aaliou3lem3  26474  aaliou3lem8  26475  sincosq1lem  26628  sincosq2sgn  26630  sincosq3sgn  26631  sincosq4sgn  26632  sinq12gt0  26638  abssinper  26652  coskpi  26654  sineq0  26655  coseq1  26656  efeq1  26659  resinf1o  26667  efif1olem2  26674  efif1olem4  26676  logneg2  26746  cxpsqrtlem  26833  cxpsqrt  26834  logsqrt  26835  1cubr  26973  leibpilem2  27072  basellem3  27213  ppiub  27334  chtublem  27341  chtub  27342  bcmax  27408  bcp1ctr  27409  bposlem2  27415  bposlem6  27419  bposlem9  27422  logdivsum  27663  elno  27776  mulscl  28293  4ipval2  31001  ipidsq  31003  dipcl  31005  dipcj  31007  ipasslem11  31133  hvmul0  31317  pjhthlem1  31684  h1de2bi  31847  spanunsni  31872  adjeu  32182  nmopge0  32204  nmfnge0  32220  opsqrlem6  32438  mdsl1i  32614  mdsl2bi  32616  mdexchi  32628  superpos  32647  atabsi  32694  dmdbr5ati  32715  cdj3lem1  32727  fpwrelmapffslem  33018  dp2cl  33140  dpfrac1  33152  cshw1s2  33221  oddpwdc  34689  eulerpartgbij  34707  subfacp1lem2a  35605  subfacp1lem5  35609  subfacp1lem6  35610  subfaclim  35613  sinccvglem  36097  dfon2lem3  36208  dfon2lem7  36212  wsuceq1  36238  clsun  36762  vtoclefex  37903  finxpreclem5  37964  sin2h  38184  cos2h  38185  tan2h  38186  poimirlem22  38216  poimirlem31  38225  opnmbllem0  38230  mblfinlem3  38233  itg2addnclem3  38247  ftc1cnnclem  38265  ftc1anclem6  38272  ftc2nc  38276  dvasin  38278  fdc  38319  constcncf  38336  heiborlem7  38391  atlatmstc  40018  lcmineqlem10  42730  lcmineqlem12  42732  facp2  42835  3rdpwhole  42978  sn-00idlem1  43084  0prjspnlem  43282  sn-isghm  43332  diophren  43467  oaabsb  43948  dftrcl3  44373  dfrtrcl3  44386  cotrclrcl  44395  lhe4.4ex1a  44966  dirkerper  46737  sinnpoly  47552  zlmodzxznm  49197  sinh-conventional  50437