Theorem mpand 711

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
mpand	|- ( ph -> ( ch -> th ) )

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 |- ( ph -> ps )
2		mpand.2	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	ancomsd 470	. 2 |- ( ph -> ( ( ch /\ ps ) -> th ) )
4	1, 3	mpan2d 710	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

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

This theorem is referenced by:  mpani  712  mp2and  715  ecase2d  981  disjss3  4652  sotri2  5525  fpropnf1  6524  ovig  6782  orduniorsuc  7030  omopth2  7664  frfi  8205  ordunifi  8210  finsschain  8273  cantnfp1lem3  8577  cantnfp1  8578  p1le  10866  nnge1  11046  zltp1le  11427  gtndiv  11454  uzss  11708  eluzadd  11716  uzm1  11718  addlelt  11942  xrre2  12001  xrre3  12002  xrmaxlt  12012  xrmaxle  12014  xrsupsslem  12137  xrub  12142  supxrunb1  12149  zltaddlt1le  12324  nn0p1elfzo  12510  elfzoext  12524  flflp1  12608  ceile  12648  modfzo0difsn  12742  seqf1olem1  12840  leexp2r  12918  expnlbnd2  12995  facavg  13088  wrdred1hash  13350  ccat2s1fvw  13415  caubnd2  14097  limsupbnd1  14213  limsupbnd2  14214  rlim2lt  14228  rlim3  14229  o1co  14317  mulcn2  14326  cn1lem  14328  rlimo1  14347  climsqz  14371  climsqz2  14372  rlimsqzlem  14379  lo1le  14382  rlimno1  14384  climsup  14400  caucvgrlem2  14405  iseraltlem2  14413  iseralt  14415  fsumabs  14533  cvgcmp  14548  cvgcmpce  14550  isumltss  14580  cvgrat  14615  ruclem9  14967  ruclem12  14970  bitsfzolem  15156  bitsfzo  15157  sadcaddlem  15179  gcdzeq  15271  algcvgblem  15290  algcvga  15292  lcmdvdsb  15326  lcmftp  15349  coprmdvdsOLD  15367  coprm  15423  eulerthlem2  15487  pclem  15543  infpn2  15617  prmreclem1  15620  prmreclem4  15623  ramtlecl  15704  prmgaplem7  15761  initoeu2  16666  lubval  16984  lublecllem  16988  glbval  16997  joinle  17014  latmlem1  17081  odmulg  17973  efginvrel2  18140  pgpfac1lem5  18478  chfacfscmul0  20663  chfacfpmmul0  20667  1stccnp  21265  qustgplem  21924  imasdsf1olem  22178  bldisj  22203  xbln0  22219  prdsbl  22296  metss2lem  22316  stdbdxmet  22320  ngptgp  22440  nghmcn  22549  icoopnst  22738  iocopnst  22739  cnllycmp  22755  iscau3  23076  cmetcaulem  23086  iscmet3lem1  23089  bcthlem4  23124  ovollb2lem  23256  ovolicc2lem3  23287  voliunlem3  23320  volcn  23374  itg10a  23477  itg1ge0a  23478  dvcnvrelem1  23780  dvfsumrlim  23794  itgsubst  23812  ulmcn  24153  ulmdvlem3  24156  mtest  24158  tanord  24284  emcllem6  24727  ftalem2  24800  chtub  24937  fsumvma2  24939  vmasum  24941  chpchtsum  24944  bcmono  25002  bclbnd  25005  bposlem1  25009  bposlem5  25013  bposlem6  25014  lgsne0  25060  gausslemma2dlem1a  25090  chtppilim  25164  dchrisumlem3  25180  pntrsumbnd2  25256  pntlemf  25294  pntlem3  25298  pntleml  25300  upgr2pthnlp  26628  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  eupth2lems  27098  grpoidinvlem3  27360  grpoideu  27363  vacn  27549  blocni  27660  ubthlem2  27727  chscllem2  28497  lnconi  28892  pjnmopi  29007  atomli  29241  sumdmdlem2  29278  cdj3lem2b  29296  xraddge02  29521  dfon2lem5  31692  dfon2lem6  31693  nosupno  31849  cgrcoml  32103  btwnconn2  32209  ltflcei  33397  poimirlem2  33411  poimirlem18  33427  poimirlem22  33431  poimirlem23  33432  poimirlem26  33435  poimirlem29  33438  poimirlem30  33439  poimirlem32  33441  heicant  33444  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  itg2addnc  33464  bddiblnc  33480  ftc1anclem6  33490  ftc1anc  33493  mettrifi  33553  geomcau  33555  equivbnd  33589  heibor1lem  33608  bfplem1  33621  bfplem2  33622  rrncmslem  33631  divrngidl  33827  lecmtN  34543  cvrletrN  34560  llnnleat  34799  lplnnle2at  34827  lvolnle3at  34868  dalem21  34980  cdlemblem  35079  osumcllem11N  35252  pexmidlem8N  35263  lhpmcvr4N  35312  cdleme32b  35730  cdleme35fnpq  35737  cdleme48bw  35790  cdlemf1  35849  cdlemg2fv2  35888  cdlemg7fvbwN  35895  cdlemg27b  35984  tendoeq2  36062  dia2dimlem1  36353  dihord6apre  36545  dihord5apre  36551  dihglbcpreN  36589  dochnel2  36681  dihjat1lem  36717  dochexmidlem8  36756  mapdordlem2  36926  frege124d  38053  climinf  39838  2ffzoeq  41338  iccpartlt  41360  lighneallem2  41523  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  tgoldbach  41705  tgoldbachOLD  41712  fllog2  42362  dignn0ldlem  42396