Theorem syl112anc 1401

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 521	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1398	1 ⊢ (𝜑 → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  rmob2  3840  2nreu  4401  fveqf1o  7314  frrlem12  8322  enfixsn  9112  gruina  10910  grur1  10912  enqeq  11026  muldivdid  12018  recrec  12021  rec11r  12023  divdivdiv  12025  dmdcan  12034  ddcan  12038  rereccl  12042  div2neg  12047  divmuld  12122  divmul2d  12133  divmul3d  12134  divassd  12135  div12d  12136  div23d  12137  divdird  12138  divsubdird  12139  div11d  12140  ltmul12a  12180  ltdiv1  12188  ltrec  12206  lt2msq1  12208  lediv2  12214  supmul1  12293  qbtwnre  13336  xlemul1a  13425  xlemul1  13427  xadd4d  13440  quoremz  14002  quoremnn0ALT  14004  expgt1  14250  nnlesq  14356  expnbnd  14383  expmulnbnd  14386  discr1  14390  facubnd  14451  pfxsuffeqwrdeq  14855  01sqrexlem6  15423  mulcn2  15772  geomulcvg  16054  cvgrat  16061  eftlub  16286  eflegeo  16298  tanhlt1  16337  sin01bnd  16362  cos01bnd  16363  eirrlem  16381  bitsmod  16615  mulgcd  16730  mulgcddvds  16839  prmind2  16869  qnumgt0  16935  pcpremul  17030  fldivp1  17084  pcfaclem  17085  qexpz  17088  prmpwdvds  17091  pockthg  17093  prmreclem1  17103  prmreclem5  17107  4sqlem10  17134  4sqlem12  17143  4sqlem16  17147  4sqlem17  17148  vdwlem3  17170  vdwlem8  17175  vdwlem9  17176  0ram  17207  ramz2  17211  cat1lem  18280  odmulg  19779  dfod2  19787  odf1o1  19795  odf1o2  19796  sylow3lem4  19853  ablsub4  20033  odadd1  20071  odadd2  20072  ablfacrp2  20292  ablfac1b  20295  ablfac1eu  20298  pgpfac1lem3a  20301  pgpfaclem2  20307  ablsimpgfindlem1  20332  chrcong  21842  znrrg  21880  cygznlem1  21881  chpdmatlem3  23167  txdis  23960  txdis1cn  23963  ptunhmeo  24136  qustgplem  24449  blcld  24833  nlmvscnlem2  25013  blcvx  25126  metds0  25179  metdseq0  25183  icopnfcnv  25272  lebnumii  25296  ipcau2  25564  tcphcphlem1  25565  ipcnlem2  25574  csbren  25729  trirn  25730  dyadf  25921  dyadovol  25923  dyaddisjlem  25925  dyadmaxlem  25927  opnmbllem  25931  mbfmulc2lem  25977  mbfi1fseqlem4  26048  mbfi1fseqlem5  26049  mbfi1fseqlem6  26050  itg2mulclem  26076  itg2monolem1  26080  itg2monolem3  26082  itg2cnlem2  26092  itgabs  26164  dvlip  26322  dvlt0  26334  dvcvx  26349  ftc1lem4  26368  dgrcolem2  26602  aaliou3lem2  26679  aaliou3lem9  26686  itgulm  26744  radcnvlem1  26749  abelthlem2  26768  abelthlem7  26774  tangtx  26843  cosne0  26866  cosordlem  26867  tanord1  26874  logdivlti  26957  logcnlem4  26982  logf1o2  26987  cxpcn3lem  27084  cxpaddle  27089  ang180lem2  27147  atanlogsublem  27252  atantan  27260  atanbndlem  27262  atans2  27268  leibpi  27279  log2tlbnd  27282  birthdaylem3  27290  efrlim  27306  jensenlem2  27324  zetacvg  27351  ftalem1  27409  ftalem5  27413  basellem1  27417  basellem4  27420  fsumdvdsdiaglem  27519  dvdsflf1o  27523  fsumfldivdiaglem  27525  ppiub  27540  mersenne  27563  dchrptlem1  27600  bposlem1  27620  bposlem2  27621  bposlem4  27623  lgsdilem  27660  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgsquadlem1  27716  lgsquadlem2  27717  2sqlem3  27756  2sqlem8  27762  2sqlem11  27765  2sqblem  27767  chebbnd1lem2  27806  chebbnd1lem3  27807  rplogsumlem1  27820  rplogsumlem2  27821  dchrisumlem1  27825  dchrmusum2  27830  dchrisum0flblem1  27844  mulog2sumlem1  27870  logdivbnd  27892  pntpbnd1a  27921  pntpbnd1  27922  pntpbnd2  27923  pntlemh  27935  pntlemr  27938  pntlemk  27942  pntlemo  27943  ostth2lem1  27954  ostth2lem2  27970  ostth2lem3  27971  ostth3  27974  noextenddif  28034  noextendlt  28035  noextendgt  28036  nosupbnd1lem3  28076  nosupbnd1lem4  28077  nosupbnd1lem5  28078  nosupbnd1lem6  28079  noinfbnd1lem3  28091  noinfbnd1lem4  28092  noinfbnd1lem5  28093  noinfbnd1lem6  28094  noetasuplem4  28102  madecut  28278  cofcut2  28317  eucliddivs  28771  legov  29057  axsegcon  29514  axpaschlem  29527  0uhgrsubgr  29869  clwwlkf1  30649  upgr4cycl4dv4e  30795  eupth2lem3lem3  30840  nrt2irr  31083  nmblolbii  31410  nmbdoplbi  32635  nmcoplbi  32639  nmophmi  32642  nmbdfnlbi  32660  nmcfnlbi  32663  cnlnadjlem7  32684  nmopcoi  32706  resf1o  33372  receqid  33386  xdivrec  33543  cycpmfvlem  33723  cycpmfv3  33726  lbsdiflsp0  34308  txomap  34516  unitdivcld  34583  measvunilem  34895  measvuni  34897  measssd  34898  measiuns  34900  measinblem  34903  measdivcst  34907  sibfof  35022  oddpwdc  35036  sseqfv1  35071  sseqfv2  35076  probun  35101  totprobd  35108  dstrvprob  35154  actfunsnrndisj  35284  reprsuc  35294  breprexplema  35309  subfaclim  36043  connpconn  36090  cvmliftlem2  36141  cvmliftlem6  36145  cvmliftlem7  36146  cvmliftlem8  36147  cvmliftlem9  36148  cvmliftlem10  36149  snmlff  36184  lineext  36937  hilbert1.1  37015  nn0prpwlem  37206  poimirlem1  38648  opnmbllem0  38683  ismblfin  38688  itgabsnc  38716  ftc1cnnclem  38718  bfplem1  38865  bfp  38867  lfl1  40236  lfladdcl  40237  eqlkr  40265  lkrlsp  40268  atcvrj2b  40598  3dim1  40633  3dim2  40634  llni2  40678  2llnjaN  40732  lvoli3  40743  lvoli2  40747  lncvrelatN  40947  lhpat4N  41210  lhpat3  41212  4atexlemex6  41240  ldilco  41282  ltrnid  41301  ltrnatb  41303  ltrnel  41305  ltrncnvel  41308  ltrncnv  41312  ltrn11at  41313  ltrneq  41315  trlat  41335  trlator0  41337  ltrnnidn  41340  trlid0  41342  trlnidatb  41343  trlnle  41352  trlval3  41353  trlval4  41354  cdlemc2  41358  cdlemc5  41361  cdlemc6  41362  cdlemc  41363  cdlemd2  41365  cdlemd9  41372  cdleme0e  41383  cdleme02N  41388  cdleme0ex1N  41389  cdleme3e  41398  cdleme3g  41400  cdleme3h  41401  cdleme3  41403  cdleme7aa  41408  cdleme7b  41410  cdleme7c  41411  cdleme7d  41412  cdleme7e  41413  cdleme7ga  41414  cdleme7  41415  cdleme9  41419  cdleme16aN  41425  cdleme11c  41427  cdleme11dN  41428  cdleme11e  41429  cdleme11h  41432  cdleme11j  41433  cdleme11k  41434  cdleme12  41437  cdleme21j  41502  cdleme26eALTN  41527  cdleme26f  41529  cdleme26f2  41531  cdlemefrs29bpre0  41562  cdleme35a  41614  cdleme35b  41616  cdleme35c  41617  cdleme35f  41620  cdleme36a  41626  cdleme38m  41629  cdlemeg46rgv  41694  cdlemeg46req  41695  cdlemf  41729  cdlemg2fvlem  41760  cdlemg2l  41769  cdlemg7N  41792  cdlemg12g  41815  cdlemg15  41822  cdlemg17h  41834  cdlemg17  41843  cdlemg19a  41849  cdlemg24  41854  cdlemg37  41855  cdlemg27a  41858  cdlemg31b0N  41860  cdlemg27b  41862  cdlemg31c  41865  cdlemg31d  41866  cdlemg35  41879  trljco  41906  tgrpgrplem  41915  cdlemh2  41982  tendoconid  41995  tendotr  41996  cdlemk35s-id  42104  cdlemk39s-id  42106  cdlemk53b  42122  cdlemk53  42123  cdlemk54  42124  cdleml3N  42144  cdleml5N  42146  tendospcanN  42189  diclss  42359  dihvalcq2  42413  dihord4  42424  dihord5b  42425  dihord5apre  42428  dihmeetlem1N  42456  dihmeetbclemN  42470  dihmeetlem20N  42492  dihmeetALTN  42493  dihatlat  42500  dihatexv  42504  dochkr1  42644  dochkr1OLDN  42645  lcfl7lem  42665  lclkrlem2m  42685  hdmaplna1  43073  hdmaplns1  43074  hdmaplnm1  43075  cxp111d  43502  eldioph2lem1  43880  fphpdo  43933  irrapxlem1  43938  irrapxlem2  43939  irrapxlem3  43940  irrapxlem5  43942  pellexlem2  43946  pell1234qrreccl  43970  pell1234qrmulcl  43971  pell1234qrdich  43977  pell1qr1  43987  pellqrexplicit  43993  pellfundex  44002  reglogltb  44007  reglogleb  44008  pellfund14  44014  rmxycomplete  44033  jm2.24nn  44075  jm2.17b  44077  jm2.17c  44078  jm2.18  44104  jm2.19lem2  44106  jm2.20nn  44113  jm2.16nn0  44120  jm3.1lem2  44134  areaquad  44327  clsk3nimkb  45149  lemuldiv3d  45279  lemuldiv4d  45280  stoweidlem1  47119  stoweidlem11  47129  stoweidlem14  47132  stoweidlem26  47144  stoweidlem34  47152  stoweidlem38  47156  stoweidlem60  47178  fourierdlem52  47276  etransclem38  47390  2tceilhalfelfzo1  48514  reuopreuprim  48716  nprmdvdsfacm1lem4  48816  quad1  48826  requad1  48828  requad2  48829  isubgr3stgrlem1  49172  isubgr3stgrlem3  49174  gpg3kgrtriexlem1  49289  gpg3kgrtriexlem5  49293  domnmsuppn0  49589  lincvalpr  49638  ldepspr  49693  islindeps2  49703  fldivexpfllog2  49785  eenglngeehlnmlem1  49958  eenglngeehlnmlem2  49959  rrx2linest  49962  prsthinc  50707