Theorem mp3an1 1411

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an1.1	|- ph
mp3an1.2	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an1	|- ( ( ps /\ ch ) -> th )

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 |- ph
2		mp3an1.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expb 1266	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	1, 3	mpan 706	1 |- ( ( ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  mp3an12  1414  mp3an1i  1417  mp3anl1  1418  mp3an  1424  mp3an2i  1429  mp3an3an  1430  onint  6995  wfrlem12  7426  wfrlem17  7431  tfrlem9  7481  oaord1  7631  oaword2  7633  oawordeulem  7634  oa00  7639  omword1  7653  omword2  7654  omlimcl  7658  oeoelem  7678  nnaordex  7718  enp1i  8195  unfilem2  8225  dffi3  8337  unbnn3  8556  pwcdaen  9007  ackbij1b  9061  zorn2  9328  zornn0  9330  ttukey  9340  brdom7disj  9353  brdom6disj  9354  wunex2  9560  muladd11  10206  00id  10211  mul02  10214  negsubdi  10337  mulneg1  10466  ltaddpos  10518  addge01  10538  reccl  10692  recid  10699  recid2  10700  recdiv2  10738  divdiv23zi  10778  ltmul12a  10879  lemul12a  10881  mulgt1  10882  ltmulgt11  10883  gt0div  10889  ge0div  10890  lediv12a  10916  ledivp1  10925  ltdiv23i  10948  ledivp1i  10949  ltdivp1i  10950  infm3  10982  nngt1ne1  11047  8th4div3  11252  gtndiv  11454  nn0ind  11472  fnn0ind  11476  supminf  11775  xrre2  12001  2resupmax  12019  qsqueeze  12032  xmulpnf1  12104  xlemul1a  12118  xrub  12142  ioorebas  12275  elfz0ubfz0  12443  expubnd  12921  le2sq2  12939  crreczi  12989  bernneq  12990  faclbnd5  13085  faclbnd6  13086  bccl  13109  hashbc  13237  wrdred1hash  13350  ccatlid  13369  shftfval  13810  sgnp  13830  mulre  13861  sqrlem4  13986  sqrlem7  13989  sqreulem  14099  binom1p  14563  0.999...OLD  14613  fallrisefac  14756  bpoly3  14789  efsub  14830  efi4p  14867  sinadd  14894  cosadd  14895  cos2t  14908  cos2tsin  14909  sin01gt0  14920  cos01gt0  14921  absefib  14928  efieq1re  14929  demoivreALT  14931  rpnnen2lem4  14946  odd2np1  15065  opoe  15087  omoe  15088  opeo  15089  omeo  15090  divalglem0  15116  divalglem4  15119  divalglem9  15124  gcdcllem3  15223  gcdn0gt0  15239  gcdadd  15247  gcdmultiple  15269  algcvgblem  15290  algcvga  15292  isprm3  15396  coprm  15423  pythagtriplem4  15524  pythagtriplem11  15530  pythagtriplem12  15531  pythagtriplem13  15532  pythagtriplem14  15533  infpn2  15617  1arith2  15632  vdwap0  15680  vdwap1  15681  ipolt  17159  gsumval2a  17279  f1otrspeq  17867  rmodislmod  18931  mplsubrglem  19439  evls1rhm  19687  cnfldneg  19772  cnflddiv  19776  cnfldmulg  19778  cnfldexp  19779  zringmulg  19826  remulg  19953  resubgval  19955  thlleval  20042  frlmsslsp  20135  neiptoptop  20935  iccordt  21018  qustgplem  21924  bl2ioo  22595  ioo2blex  22597  blssioo  22598  tgioo  22599  xrsblre  22614  iccntr  22624  icccmplem3  22627  reconnlem2  22630  opnreen  22634  iccpnfcnv  22743  cnllycmp  22755  pcoptcl  22821  ovolmge0  23245  ovolctb2  23260  ismbl2  23295  cmmbl  23302  nulmbl  23303  unmbl  23305  voliunlem1  23318  voliunlem2  23319  ioombl1  23330  opnmbllem  23369  mbfima  23399  i1fsub  23475  itg1sub  23476  ellimc3  23643  limcflf  23645  dvcnvre  23782  coe1termlem  24014  dgrsub  24028  dvnply2  24042  dvnply  24043  reeff1o  24201  sinperlem  24232  sincosq1eq  24264  resinf1o  24282  logeftb  24330  logge0  24351  logdivlti  24366  efopn  24404  logtayl2  24408  loglesqrt  24499  logrec  24501  xrlimcnp  24695  ppinncl  24900  chtrpcl  24901  bposlem2  25010  bposlem8  25016  lgsdir2  25055  1lgs  25065  brbtwn2  25785  colinearalglem4  25789  ax5seglem1  25808  ax5seglem2  25809  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  fusgrfis  26222  3cyclfrgrrn  27150  isgrpoi  27352  imsmetlem  27545  nmcvcn  27550  ipval2  27562  lnocoi  27612  nmlno0lem  27648  nmblolbii  27654  blometi  27658  blocnilem  27659  blocni  27660  ipasslem1  27686  ipasslem2  27687  ipasslem4  27689  ipasslem5  27690  ipasslem8  27692  ipblnfi  27711  ip2eqi  27712  ubthlem1  27726  htthlem  27774  h2hmetdval  27835  axhvcom-zf  27840  axhis1-zf  27851  axhis4-zf  27854  hvm1neg  27889  hvsub4  27894  hvsubass  27901  hvsubdistr2  27907  hv2times  27918  hvsubcan  27931  hvsubcan2  27932  his2sub  27949  norm-i  27986  normpyc  28003  hhip  28034  hhph  28035  norm1exi  28107  hhssabloilem  28118  hhssnv  28121  hhshsslem2  28125  hhssmetdval  28135  shscli  28176  shunssi  28227  shsleji  28229  shsidmi  28243  spanunsni  28438  h1datomi  28440  spansncvi  28511  pjss2i  28539  pjssmii  28540  pjocini  28557  homulid2  28659  honegdi  28668  ho2times  28678  nmopge0  28770  nmopgt0  28771  nmfnge0  28786  lnopaddi  28830  lnopmuli  28831  lnopsubi  28833  hmopbdoptHIL  28847  nmbdoplbi  28883  nmcoplbi  28887  nmophmi  28890  lnopconi  28893  lnfnaddi  28902  lnfnsubi  28905  nmbdfnlbi  28908  nmcfnlbi  28911  lnfnconi  28914  imaelshi  28917  cnlnadjlem2  28927  cnlnadjlem7  28932  nmoptrii  28953  nmopcoi  28954  adjcoi  28959  nmopcoadji  28960  bracnlnval  28973  leopmul  28993  opsqrlem1  28999  opsqrlem6  29004  hmopidmpji  29011  sto2i  29096  strlem1  29109  atcveq0  29207  atcv0eq  29238  atomli  29241  atcvati  29245  atcvat3i  29255  cdjreui  29291  cdj1i  29292  xdiv0  29637  xdivpnfrp  29641  mhmhmeotmd  29973  rezh  30015  qqhucn  30036  blsconn  31226  cnllysconn  31227  sinccvglem  31566  frrlem11  31792  nosupno  31849  nosupbday  31851  noetalem3  31865  opnrebl2  32316  ptrecube  33409  poimirlem6  33415  poimirlem7  33416  poimirlem29  33438  poimirlem30  33439  opnmbllem0  33445  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  voliunnfl  33453  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  heiborlem7  33616  rrnequiv  33634  ismrer1  33637  el3v1  33988  cnaddcom  34259  mapco2  37278  mzpaddmpt  37304  mzpmulmpt  37305  zindbi  37511  mpaaeu  37720  eel000cT  38928  eel0TT  38929  supminfxr  39694  fmtno4prmfac  41484  zringsubgval  42183  aacllem  42547