Theorem syl112anc 1354

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

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl112anc.5	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl112anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl112anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 504	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1351	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  rmob2  3780  2nreu  4276  fveqf1o  6883  enfixsn  8422  gruina  10038  grur1  10040  enqeq  10154  recrec  11138  rec11r  11140  divdivdiv  11142  dmdcan  11151  ddcan  11155  rereccl  11159  div2neg  11164  divmuld  11239  divmul2d  11250  divmul3d  11251  divassd  11252  div12d  11253  div23d  11254  divdird  11255  divsubdird  11256  div11d  11257  ltmul12a  11297  ltdiv1  11305  ltrec  11323  lt2msq1  11325  lediv2  11331  supmul1  11411  qbtwnre  12409  xlemul1a  12497  xlemul1  12499  xadd4d  12512  quoremz  13038  quoremnn0ALT  13040  expgt1  13282  nnlesq  13383  expnbnd  13408  expmulnbnd  13411  discr1  13415  facubnd  13475  hashf1lem1  13626  2swrdeqwrdeqOLD  13846  pfxsuffeqwrdeq  13880  sqrlem6  14468  mulcn2  14813  geomulcvg  15092  cvgrat  15099  eftlub  15322  eflegeo  15334  tanhlt1  15373  sin01bnd  15398  cos01bnd  15399  eirrlem  15417  bitsmod  15645  mulgcd  15752  mulgcddvds  15855  prmind2  15885  qnumgt0  15946  pcpremul  16036  fldivp1  16089  pcfaclem  16090  qexpz  16093  prmpwdvds  16096  pockthg  16098  prmreclem1  16108  prmreclem5  16112  4sqlem10  16139  4sqlem12  16148  4sqlem16  16152  4sqlem17  16153  vdwlem3  16175  vdwlem8  16180  vdwlem9  16181  0ram  16212  ramz2  16216  xpsc0  16689  xpsc1  16690  odmulg  18444  dfod2  18452  odf1o1  18458  odf1o2  18459  sylow3lem4  18516  ablsub4  18691  odadd1  18724  odadd2  18725  ablfacrp2  18939  ablfac1b  18942  ablfac1eu  18945  pgpfac1lem3a  18948  pgpfaclem2  18954  chrcong  20378  znrrg  20414  cygznlem1  20415  chpdmatlem3  21152  txdis  21944  txdis1cn  21947  ptunhmeo  22120  qustgplem  22432  blcld  22818  nlmvscnlem2  22997  blcvx  23109  metds0  23161  metdseq0  23165  icopnfcnv  23249  lebnumii  23273  ipcau2  23540  tcphcphlem1  23541  ipcnlem2  23550  csbren  23705  trirn  23706  dyadf  23895  dyadovol  23897  dyaddisjlem  23899  dyadmaxlem  23901  opnmbllem  23905  mbfmulc2lem  23951  mbfi1fseqlem4  24022  mbfi1fseqlem5  24023  mbfi1fseqlem6  24024  itg2mulclem  24050  itg2monolem1  24054  itg2monolem3  24056  itg2cnlem2  24066  itgabs  24138  dvlip  24293  dvlt0  24305  dvcvx  24320  ftc1lem4  24339  dgrcolem2  24567  aaliou3lem2  24635  aaliou3lem9  24642  itgulm  24699  radcnvlem1  24704  abelthlem2  24723  abelthlem7  24729  tangtx  24794  cosne0  24815  cosordlem  24816  tanord1  24822  logdivlti  24904  logcnlem4  24929  logf1o2  24934  cxpcn3lem  25029  cxpaddle  25034  ang180lem2  25089  atanlogsublem  25194  atantan  25202  atanbndlem  25204  atans2  25210  leibpi  25222  log2tlbnd  25225  birthdaylem3  25233  efrlim  25249  jensenlem2  25267  zetacvg  25294  ftalem1  25352  ftalem5  25356  basellem1  25360  basellem4  25363  fsumdvdsdiaglem  25462  dvdsflf1o  25466  fsumfldivdiaglem  25468  ppiub  25482  mersenne  25505  dchrptlem1  25542  bposlem1  25562  bposlem2  25563  bposlem4  25565  lgsdilem  25602  lgseisenlem1  25653  lgseisenlem2  25654  lgseisenlem3  25655  lgsquadlem1  25658  lgsquadlem2  25659  2sqlem3  25698  2sqlem8  25704  2sqlem11  25707  2sqblem  25709  chebbnd1lem2  25748  chebbnd1lem3  25749  rplogsumlem1  25762  rplogsumlem2  25763  dchrisumlem1  25767  dchrmusum2  25772  dchrisum0flblem1  25786  mulog2sumlem1  25812  logdivbnd  25834  pntpbnd1a  25863  pntpbnd1  25864  pntpbnd2  25865  pntlemh  25877  pntlemr  25880  pntlemk  25884  pntlemo  25885  ostth2lem1  25896  ostth2lem2  25912  ostth2lem3  25913  ostth3  25916  legov  26073  axsegcon  26416  axpaschlem  26429  0uhgrsubgr  26764  clwwlkf1OLD  27566  clwwlkf1  27571  upgr4cycl4dv4e  27714  eupth2lem3lem3  27760  nmblolbii  28353  nmbdoplbi  29582  nmcoplbi  29586  nmophmi  29589  nmbdfnlbi  29607  nmcfnlbi  29610  cnlnadjlem7  29631  nmopcoi  29653  resf1o  30218  xdivrec  30349  cycpmfv1  30444  cycpmfv2  30445  cycpmfv3  30446  lbsdiflsp0  30648  txomap  30739  unitdivcld  30785  measvunilem  31113  measvuni  31115  measssd  31116  measiuns  31118  measinblem  31121  measdivcst  31126  sibfof  31240  oddpwdc  31254  sseqfv1  31290  sseqfv2  31295  probun  31320  totprobd  31327  dstrvprob  31372  actfunsnrndisj  31521  reprsuc  31531  breprexplema  31546  subfaclim  32017  connpconn  32064  cvmliftlem2  32115  cvmliftlem6  32119  cvmliftlem7  32120  cvmliftlem8  32121  cvmliftlem9  32122  cvmliftlem10  32123  snmlff  32158  frrlem12  32652  noextenddif  32693  noextendlt  32694  noextendgt  32695  nosupbnd1lem3  32728  nosupbnd1lem4  32729  nosupbnd1lem5  32730  nosupbnd1lem6  32731  noetalem3  32737  lineext  33055  hilbert1.1  33133  nn0prpwlem  33188  poimirlem1  34331  opnmbllem0  34366  ismblfin  34371  itgabsnc  34399  ftc1cnnclem  34403  bfplem1  34539  bfp  34541  lfl1  35648  lfladdcl  35649  eqlkr  35677  lkrlsp  35680  atcvrj2b  36010  3dim1  36045  3dim2  36046  llni2  36090  2llnjaN  36144  lvoli3  36155  lvoli2  36159  lncvrelatN  36359  lhpat4N  36622  lhpat3  36624  4atexlemex6  36652  ldilco  36694  ltrnid  36713  ltrnatb  36715  ltrnel  36717  ltrncnvel  36720  ltrncnv  36724  ltrn11at  36725  ltrneq  36727  trlat  36747  trlator0  36749  ltrnnidn  36752  trlid0  36754  trlnidatb  36755  trlnle  36764  trlval3  36765  trlval4  36766  cdlemc2  36770  cdlemc5  36773  cdlemc6  36774  cdlemc  36775  cdlemd2  36777  cdlemd9  36784  cdleme0e  36795  cdleme02N  36800  cdleme0ex1N  36801  cdleme3e  36810  cdleme3g  36812  cdleme3h  36813  cdleme3  36815  cdleme7aa  36820  cdleme7b  36822  cdleme7c  36823  cdleme7d  36824  cdleme7e  36825  cdleme7ga  36826  cdleme7  36827  cdleme9  36831  cdleme16aN  36837  cdleme11c  36839  cdleme11dN  36840  cdleme11e  36841  cdleme11h  36844  cdleme11j  36845  cdleme11k  36846  cdleme12  36849  cdleme21j  36914  cdleme26eALTN  36939  cdleme26f  36941  cdleme26f2  36943  cdlemefrs29bpre0  36974  cdleme35a  37026  cdleme35b  37028  cdleme35c  37029  cdleme35f  37032  cdleme36a  37038  cdleme38m  37041  cdlemeg46rgv  37106  cdlemeg46req  37107  cdlemf  37141  cdlemg2fvlem  37172  cdlemg2l  37181  cdlemg7N  37204  cdlemg12g  37227  cdlemg15  37234  cdlemg17h  37246  cdlemg17  37255  cdlemg19a  37261  cdlemg24  37266  cdlemg37  37267  cdlemg27a  37270  cdlemg31b0N  37272  cdlemg27b  37274  cdlemg31c  37277  cdlemg31d  37278  cdlemg35  37291  trljco  37318  tgrpgrplem  37327  cdlemh2  37394  tendoconid  37407  tendotr  37408  cdlemk35s-id  37516  cdlemk39s-id  37518  cdlemk53b  37534  cdlemk53  37535  cdlemk54  37536  cdleml3N  37556  cdleml5N  37558  tendospcanN  37601  diclss  37771  dihvalcq2  37825  dihord4  37836  dihord5b  37837  dihord5apre  37840  dihmeetlem1N  37868  dihmeetbclemN  37882  dihmeetlem20N  37904  dihmeetALTN  37905  dihatlat  37912  dihatexv  37916  dochkr1  38056  dochkr1OLDN  38057  lcfl7lem  38077  lclkrlem2m  38097  hdmaplna1  38485  hdmaplns1  38486  hdmaplnm1  38487  eldioph2lem1  38749  fphpdo  38807  irrapxlem1  38812  irrapxlem2  38813  irrapxlem3  38814  irrapxlem5  38816  pellexlem2  38820  pell1234qrreccl  38844  pell1234qrmulcl  38845  pell1234qrdich  38851  pell1qr1  38861  pellqrexplicit  38867  pellfundex  38876  reglogltb  38881  reglogleb  38882  pellfund14  38888  rmxycomplete  38907  jm2.24nn  38949  jm2.17b  38951  jm2.17c  38952  jm2.18  38978  jm2.19lem2  38980  jm2.20nn  38987  jm2.16nn0  38994  jm3.1lem2  39008  areaquad  39216  clsk3nimkb  39750  lemuldiv3d  39884  lemuldiv4d  39885  ablsimpgfindlem1  40040  stoweidlem1  41715  stoweidlem11  41725  stoweidlem14  41728  stoweidlem26  41740  stoweidlem34  41748  stoweidlem38  41752  stoweidlem60  41774  fourierdlem52  41872  etransclem38  41986  reuopreuprim  43054  quad1  43151  requad1  43153  requad2  43154  domnmsuppn0  43781  lincvalpr  43838  ldepspr  43893  islindeps2  43903  fldivexpfllog2  43991  eenglngeehlnmlem1  44090  eenglngeehlnmlem2  44091  rrx2linest  44095