Theorem syl2anc 642

Description: Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)

Hypotheses

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

Assertion

Ref	Expression
syl2anc	|- (ph -> th)

Proof of Theorem syl2anc

Step	Hyp	Ref	Expression
1		syl2anc.1	. 2 |- (ph -> ps)
2		syl2anc.2	. 2 |- (ph -> ch)
3		syl2anc.3	. . 3 |- ((ps /\ ch) -> th)
4	3	ex 423	. 2 |- (ps -> (ch -> th))
5	1, 2, 4	sylc 56	1 |- (ph -> th)

Syntax hints:   -> wi 4   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  sylancl  643  sylancr  644  sylancom  648  mpdan  649  mpancom  650  orim12d  811  syl13anc  1184  syl31anc  1185  nanbi12d  1303  nfimdOLD  1809  ax11indalem  2197  ax11inda2ALT  2198  eqeq12d  2367  rsp2e  2678  eueq2  3011  csbiedf  3174  nineq12d  3243  symdifeq12d  3257  sstrd  3283  psstrd  3377  sspsstrd  3378  psssstrd  3379  uneq12d  3420  unssd  3440  ineq12d  3459  ssind  3480  preq12d  3808  opkeq12d  4068  symdifexg  4104  pwadjoin  4120  xpkeq12d  4207  sspw1  4336  addceq12d  4392  preaddccan2  4456  leltfintr  4459  ltfintri  4467  ncfinprop  4475  ncfindi  4476  ncfinraise  4482  ncfinlower  4484  tfindi  4497  tfinsuc  4499  tfinltfinlem1  4501  tfinltfin  4502  eventfin  4518  oddtfin  4519  nnadjoin  4521  sfindbl  4531  sfintfin  4533  tfinnn  4535  sfinltfin  4536  1cvsfin  4543  vfintle  4547  vfinspsslem1  4551  vfinspclt  4553  vinf  4556  nfopd  4606  breq12d  4653  xpeq12d  4810  nfimad  4955  funprgOLD  5151  funfni  5184  fnunsn  5191  feq23d  5221  fssxp  5233  fconstg  5252  f1ores  5301  resdif  5307  nffvd  5336  fvelimab  5371  eqfnfvd  5396  fimacnv  5412  foco2  5427  ffvresb  5432  fconst3  5458  isores2  5494  f1oiso2  5501  oveq12d  5541  mpteq12dv  5657  fmpt2d  5696  fvmptd  5703  fullfunexg  5860  trrd  5926  refrd  5927  antird  5929  antid  5930  connexrd  5931  connexd  5932  iserd  5943  xpsnen2g  6055  nenpw1pwlem2  6086  nntccl  6171  ltcpw1pwg  6203  sbthlem1  6204  sbthlem3  6206  sbth  6207  dflec3  6222  nclenc  6223  lenc  6224  tcncg  6225  tlecg  6231  nclenn  6250  addcdir  6252  lemuc1  6254  lemuc2  6255  nnltp1c  6263  addccan2nc  6266  lecadd2  6267  ncslesuc  6268  nmembers1lem3  6271  spaccl  6287  nchoicelem1  6290  nchoicelem2  6291  nchoicelem9  6298  nchoicelem12  6301  nchoicelem13  6302  nchoicelem17  6306  nchoicelem19  6308  nchoice  6309  fnfreclem1  6318  fnfreclem3  6320  frecsuc  6323