Theorem syl112anc 1372

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  rmob2  3829  2nreu  4380  fveqf1o  7168  frrlem12  8097  enfixsn  8837  gruina  10558  grur1  10560  enqeq  10674  recrec  11655  rec11r  11657  divdivdiv  11659  dmdcan  11668  ddcan  11672  rereccl  11676  div2neg  11681  divmuld  11756  divmul2d  11767  divmul3d  11768  divassd  11769  div12d  11770  div23d  11771  divdird  11772  divsubdird  11773  div11d  11774  ltmul12a  11814  ltdiv1  11822  ltrec  11840  lt2msq1  11842  lediv2  11848  supmul1  11927  qbtwnre  12915  xlemul1a  13004  xlemul1  13006  xadd4d  13019  quoremz  13556  quoremnn0ALT  13558  expgt1  13802  nnlesq  13903  expnbnd  13928  expmulnbnd  13931  discr1  13935  facubnd  13995  pfxsuffeqwrdeq  14392  sqrlem6  14940  mulcn2  15286  geomulcvg  15569  cvgrat  15576  eftlub  15799  eflegeo  15811  tanhlt1  15850  sin01bnd  15875  cos01bnd  15876  eirrlem  15894  bitsmod  16124  mulgcd  16237  mulgcddvds  16341  prmind2  16371  qnumgt0  16435  pcpremul  16525  fldivp1  16579  pcfaclem  16580  qexpz  16583  prmpwdvds  16586  pockthg  16588  prmreclem1  16598  prmreclem5  16602  4sqlem10  16629  4sqlem12  16638  4sqlem16  16642  4sqlem17  16643  vdwlem3  16665  vdwlem8  16670  vdwlem9  16671  0ram  16702  ramz2  16706  cat1lem  17792  odmulg  19144  dfod2  19152  odf1o1  19158  odf1o2  19159  sylow3lem4  19216  ablsub4  19395  odadd1  19430  odadd2  19431  ablfacrp2  19651  ablfac1b  19654  ablfac1eu  19657  pgpfac1lem3a  19660  pgpfaclem2  19666  ablsimpgfindlem1  19691  chrcong  20714  znrrg  20754  cygznlem1  20755  chpdmatlem3  21970  txdis  22764  txdis1cn  22767  ptunhmeo  22940  qustgplem  23253  blcld  23642  nlmvscnlem2  23830  blcvx  23942  metds0  23994  metdseq0  23998  icopnfcnv  24086  lebnumii  24110  ipcau2  24379  tcphcphlem1  24380  ipcnlem2  24389  csbren  24544  trirn  24545  dyadf  24736  dyadovol  24738  dyaddisjlem  24740  dyadmaxlem  24742  opnmbllem  24746  mbfmulc2lem  24792  mbfi1fseqlem4  24864  mbfi1fseqlem5  24865  mbfi1fseqlem6  24866  itg2mulclem  24892  itg2monolem1  24896  itg2monolem3  24898  itg2cnlem2  24908  itgabs  24980  dvlip  25138  dvlt0  25150  dvcvx  25165  ftc1lem4  25184  dgrcolem2  25416  aaliou3lem2  25484  aaliou3lem9  25491  itgulm  25548  radcnvlem1  25553  abelthlem2  25572  abelthlem7  25578  tangtx  25643  cosne0  25666  cosordlem  25667  tanord1  25674  logdivlti  25756  logcnlem4  25781  logf1o2  25786  cxpcn3lem  25881  cxpaddle  25886  ang180lem2  25941  atanlogsublem  26046  atantan  26054  atanbndlem  26056  atans2  26062  leibpi  26073  log2tlbnd  26076  birthdaylem3  26084  efrlim  26100  jensenlem2  26118  zetacvg  26145  ftalem1  26203  ftalem5  26207  basellem1  26211  basellem4  26214  fsumdvdsdiaglem  26313  dvdsflf1o  26317  fsumfldivdiaglem  26319  ppiub  26333  mersenne  26356  dchrptlem1  26393  bposlem1  26413  bposlem2  26414  bposlem4  26416  lgsdilem  26453  lgseisenlem1  26504  lgseisenlem2  26505  lgseisenlem3  26506  lgsquadlem1  26509  lgsquadlem2  26510  2sqlem3  26549  2sqlem8  26555  2sqlem11  26558  2sqblem  26560  chebbnd1lem2  26599  chebbnd1lem3  26600  rplogsumlem1  26613  rplogsumlem2  26614  dchrisumlem1  26618  dchrmusum2  26623  dchrisum0flblem1  26637  mulog2sumlem1  26663  logdivbnd  26685  pntpbnd1a  26714  pntpbnd1  26715  pntpbnd2  26716  pntlemh  26728  pntlemr  26731  pntlemk  26735  pntlemo  26736  ostth2lem1  26747  ostth2lem2  26763  ostth2lem3  26764  ostth3  26767  legov  26927  axsegcon  27276  axpaschlem  27289  0uhgrsubgr  27627  clwwlkf1  28392  upgr4cycl4dv4e  28528  eupth2lem3lem3  28573  nmblolbii  29140  nmbdoplbi  30365  nmcoplbi  30369  nmophmi  30372  nmbdfnlbi  30390  nmcfnlbi  30393  cnlnadjlem7  30414  nmopcoi  30436  resf1o  31044  xdivrec  31180  cycpmfvlem  31358  cycpmfv3  31361  lbsdiflsp0  31686  txomap  31763  unitdivcld  31830  measvunilem  32159  measvuni  32161  measssd  32162  measiuns  32164  measinblem  32167  measdivcst  32171  sibfof  32286  oddpwdc  32300  sseqfv1  32335  sseqfv2  32340  probun  32365  totprobd  32372  dstrvprob  32417  actfunsnrndisj  32564  reprsuc  32574  breprexplema  32589  subfaclim  33129  connpconn  33176  cvmliftlem2  33227  cvmliftlem6  33231  cvmliftlem7  33232  cvmliftlem8  33233  cvmliftlem9  33234  cvmliftlem10  33235  snmlff  33270  noextenddif  33850  noextendlt  33851  noextendgt  33852  nosupbnd1lem3  33892  nosupbnd1lem4  33893  nosupbnd1lem5  33894  nosupbnd1lem6  33895  noinfbnd1lem3  33907  noinfbnd1lem4  33908  noinfbnd1lem5  33909  noinfbnd1lem6  33910  noetasuplem4  33918  madecut  34044  cofcut2  34070  lineext  34357  hilbert1.1  34435  nn0prpwlem  34490  poimirlem1  35757  opnmbllem0  35792  ismblfin  35797  itgabsnc  35825  ftc1cnnclem  35827  bfplem1  35959  bfp  35961  lfl1  37063  lfladdcl  37064  eqlkr  37092  lkrlsp  37095  atcvrj2b  37425  3dim1  37460  3dim2  37461  llni2  37505  2llnjaN  37559  lvoli3  37570  lvoli2  37574  lncvrelatN  37774  lhpat4N  38037  lhpat3  38039  4atexlemex6  38067  ldilco  38109  ltrnid  38128  ltrnatb  38130  ltrnel  38132  ltrncnvel  38135  ltrncnv  38139  ltrn11at  38140  ltrneq  38142  trlat  38162  trlator0  38164  ltrnnidn  38167  trlid0  38169  trlnidatb  38170  trlnle  38179  trlval3  38180  trlval4  38181  cdlemc2  38185  cdlemc5  38188  cdlemc6  38189  cdlemc  38190  cdlemd2  38192  cdlemd9  38199  cdleme0e  38210  cdleme02N  38215  cdleme0ex1N  38216  cdleme3e  38225  cdleme3g  38227  cdleme3h  38228  cdleme3  38230  cdleme7aa  38235  cdleme7b  38237  cdleme7c  38238  cdleme7d  38239  cdleme7e  38240  cdleme7ga  38241  cdleme7  38242  cdleme9  38246  cdleme16aN  38252  cdleme11c  38254  cdleme11dN  38255  cdleme11e  38256  cdleme11h  38259  cdleme11j  38260  cdleme11k  38261  cdleme12  38264  cdleme21j  38329  cdleme26eALTN  38354  cdleme26f  38356  cdleme26f2  38358  cdlemefrs29bpre0  38389  cdleme35a  38441  cdleme35b  38443  cdleme35c  38444  cdleme35f  38447  cdleme36a  38453  cdleme38m  38456  cdlemeg46rgv  38521  cdlemeg46req  38522  cdlemf  38556  cdlemg2fvlem  38587  cdlemg2l  38596  cdlemg7N  38619  cdlemg12g  38642  cdlemg15  38649  cdlemg17h  38661  cdlemg17  38670  cdlemg19a  38676  cdlemg24  38681  cdlemg37  38682  cdlemg27a  38685  cdlemg31b0N  38687  cdlemg27b  38689  cdlemg31c  38692  cdlemg31d  38693  cdlemg35  38706  trljco  38733  tgrpgrplem  38742  cdlemh2  38809  tendoconid  38822  tendotr  38823  cdlemk35s-id  38931  cdlemk39s-id  38933  cdlemk53b  38949  cdlemk53  38950  cdlemk54  38951  cdleml3N  38971  cdleml5N  38973  tendospcanN  39016  diclss  39186  dihvalcq2  39240  dihord4  39251  dihord5b  39252  dihord5apre  39255  dihmeetlem1N  39283  dihmeetbclemN  39297  dihmeetlem20N  39319  dihmeetALTN  39320  dihatlat  39327  dihatexv  39331  dochkr1  39471  dochkr1OLDN  39472  lcfl7lem  39492  lclkrlem2m  39512  hdmaplna1  39900  hdmaplns1  39901  hdmaplnm1  39902  eldioph2lem1  40562  fphpdo  40619  irrapxlem1  40624  irrapxlem2  40625  irrapxlem3  40626  irrapxlem5  40628  pellexlem2  40632  pell1234qrreccl  40656  pell1234qrmulcl  40657  pell1234qrdich  40663  pell1qr1  40673  pellqrexplicit  40679  pellfundex  40688  reglogltb  40693  reglogleb  40694  pellfund14  40700  rmxycomplete  40719  jm2.24nn  40761  jm2.17b  40763  jm2.17c  40764  jm2.18  40790  jm2.19lem2  40792  jm2.20nn  40799  jm2.16nn0  40806  jm3.1lem2  40820  areaquad  41027  clsk3nimkb  41603  lemuldiv3d  41734  lemuldiv4d  41735  stoweidlem1  43496  stoweidlem11  43506  stoweidlem14  43509  stoweidlem26  43521  stoweidlem34  43529  stoweidlem38  43533  stoweidlem60  43555  fourierdlem52  43653  etransclem38  43767  reuopreuprim  44930  quad1  45024  requad1  45026  requad2  45027  domnmsuppn0  45657  lincvalpr  45711  ldepspr  45766  islindeps2  45776  fldivexpfllog2  45863  eenglngeehlnmlem1  46035  eenglngeehlnmlem2  46036  rrx2linest  46040  prsthinc  46287