Theorem mp3an23 1455

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  sbciegf  3804  predeq1  6292  wrecseq1  8315  ac6sfi  9290  unfilem1  9313  fiint  9336  ordtypelem2  9531  infxpenc2  10034  dju0en  10188  cfsmolem  10282  axdc4lem  10467  1nqenq  10974  mul02lem1  11409  muleqadd  11879  2halves  12457  halfcl  12465  rehalfcl  12466  half0  12467  halfpos2  12468  halfnneg2  12470  halfaddsub  12472  nneo  12675  zeo  12677  peano5uzi  12680  fztp  13595  uzrdgxfr  13983  bcn2  14335  bcpasc  14337  hashxplem  14449  hashfun  14453  swrds2  14957  repsw2  14967  repsw3  14968  imre  15125  reim  15126  crim  15132  addcj  15165  imval2  15168  cnpart  15257  01sqrexlem7  15265  absmax  15346  binomfallfaclem2  16054  bpoly2  16071  bpoly3  16072  fsumcube  16074  efgt0  16119  sinf  16140  efi4p  16153  resin4p  16154  recos4p  16155  sinneg  16162  efival  16168  cosadd  16181  sinmul  16188  sinbnd  16196  cosbnd  16197  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  sin01gt0  16206  cos01gt0  16207  sin02gt0  16208  rpnnen2lem11  16240  rpnnen2lem12  16241  odd2np1lem  16357  odd2np1  16358  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem15  16847  pythagtriplem16  16848  pythagtriplem17  16849  pockthi  16925  prmreclem5  16938  prmreclem6  16939  prmlem0  17123  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  isghm  19196  odinf  19542  lbsexg  21123  psgnghm2  21539  mopnex  24456  tngnm  24588  tngngp2  24589  tngngpd  24590  tngngp  24591  addccncf  24859  sub1cncf  24861  sub2cncf  24862  iihalf1  24874  iihalf2  24877  pjthlem1  25387  ovolunlem1a  25447  ovolunlem1  25448  opnmbllem  25552  vitalilem4  25562  iblcnlem1  25739  itgcnlem  25741  dvmptre  25923  dvmptim  25924  dvlipcn  25949  mdegldg  26021  aaliou3lem3  26302  aaliou3lem8  26303  sincosq1lem  26456  sincosq2sgn  26458  sincosq3sgn  26459  sincosq4sgn  26460  sinq12gt0  26466  abssinper  26480  coskpi  26482  sineq0  26483  coseq1  26484  efeq1  26487  resinf1o  26495  efif1olem2  26502  efif1olem4  26504  logneg2  26574  cxpsqrtlem  26661  cxpsqrt  26662  logsqrt  26663  1cubr  26802  leibpilem2  26901  basellem3  27043  ppiub  27165  chtublem  27172  chtub  27173  bcmax  27239  bcp1ctr  27240  bposlem2  27246  bposlem6  27250  bposlem9  27253  logdivsum  27494  elno  27607  mulscl  28077  4ipval2  30635  ipidsq  30637  dipcl  30639  dipcj  30641  ipasslem11  30767  hvmul0  30951  pjhthlem1  31318  h1de2bi  31481  spanunsni  31506  adjeu  31816  nmopge0  31838  nmfnge0  31854  opsqrlem6  32072  mdsl1i  32248  mdsl2bi  32250  mdexchi  32262  superpos  32281  atabsi  32328  dmdbr5ati  32349  cdj3lem1  32361  fpwrelmapffslem  32655  dp2cl  32800  dpfrac1  32812  cshw1s2  32882  ogrpaddlt  33031  ofldlt1  33281  ofldchr  33282  oddpwdc  34332  eulerpartgbij  34350  subfacp1lem2a  35148  subfacp1lem5  35152  subfacp1lem6  35153  subfaclim  35156  sinccvglem  35640  dfon2lem3  35749  dfon2lem7  35753  wsuceq1  35779  clsun  36292  vtoclefex  37298  finxpreclem5  37359  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem22  37612  poimirlem31  37621  opnmbllem0  37626  mblfinlem3  37629  itg2addnclem3  37643  ftc1cnnclem  37661  ftc1anclem6  37668  ftc2nc  37672  dvasin  37674  fdc  37715  constcncf  37732  heiborlem7  37787  atlatmstc  39283  lcmineqlem10  41997  lcmineqlem12  41999  facp2  42102  fac2xp3  42198  sn-00idlem1  42388  0prjspnlem  42593  sn-isghm  42643  diophren  42783  oaabsb  43265  dftrcl3  43691  dfrtrcl3  43704  cotrclrcl  43713  lhe4.4ex1a  44301  dirkerper  46073  zlmodzxznm  48421  sinh-conventional  49551