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  4402  fveqf1o  7308  frrlem12  8308  enfixsn  9098  gruina  10896  grur1  10898  enqeq  11012  muldivdid  12004  recrec  12007  rec11r  12009  divdivdiv  12011  dmdcan  12020  ddcan  12024  rereccl  12028  div2neg  12033  divmuld  12108  divmul2d  12119  divmul3d  12120  divassd  12121  div12d  12122  div23d  12123  divdird  12124  divsubdird  12125  div11d  12126  ltmul12a  12166  ltdiv1  12174  ltrec  12192  lt2msq1  12194  lediv2  12200  supmul1  12279  qbtwnre  13322  xlemul1a  13411  xlemul1  13413  xadd4d  13426  quoremz  13988  quoremnn0ALT  13990  expgt1  14236  nnlesq  14342  expnbnd  14369  expmulnbnd  14372  discr1  14376  facubnd  14437  pfxsuffeqwrdeq  14840  01sqrexlem6  15407  mulcn2  15756  geomulcvg  16038  cvgrat  16045  eftlub  16270  eflegeo  16282  tanhlt1  16321  sin01bnd  16346  cos01bnd  16347  eirrlem  16365  bitsmod  16599  mulgcd  16714  mulgcddvds  16823  prmind2  16853  qnumgt0  16919  pcpremul  17014  fldivp1  17068  pcfaclem  17069  qexpz  17072  prmpwdvds  17075  pockthg  17077  prmreclem1  17087  prmreclem5  17091  4sqlem10  17118  4sqlem12  17127  4sqlem16  17131  4sqlem17  17132  vdwlem3  17154  vdwlem8  17159  vdwlem9  17160  0ram  17191  ramz2  17195  cat1lem  18264  odmulg  19763  dfod2  19771  odf1o1  19779  odf1o2  19780  sylow3lem4  19837  ablsub4  20017  odadd1  20055  odadd2  20056  ablfacrp2  20276  ablfac1b  20279  ablfac1eu  20282  pgpfac1lem3a  20285  pgpfaclem2  20291  ablsimpgfindlem1  20316  chrcong  21826  znrrg  21864  cygznlem1  21865  chpdmatlem3  23151  txdis  23944  txdis1cn  23947  ptunhmeo  24120  qustgplem  24433  blcld  24817  nlmvscnlem2  24997  blcvx  25110  metds0  25163  metdseq0  25167  icopnfcnv  25256  lebnumii  25280  ipcau2  25548  tcphcphlem1  25549  ipcnlem2  25558  csbren  25713  trirn  25714  dyadf  25905  dyadovol  25907  dyaddisjlem  25909  dyadmaxlem  25911  opnmbllem  25915  mbfmulc2lem  25961  mbfi1fseqlem4  26032  mbfi1fseqlem5  26033  mbfi1fseqlem6  26034  itg2mulclem  26060  itg2monolem1  26064  itg2monolem3  26066  itg2cnlem2  26076  itgabs  26148  dvlip  26306  dvlt0  26318  dvcvx  26333  ftc1lem4  26352  dgrcolem2  26586  aaliou3lem2  26663  aaliou3lem9  26670  itgulm  26728  radcnvlem1  26733  abelthlem2  26752  abelthlem7  26758  tangtx  26827  cosne0  26850  cosordlem  26851  tanord1  26858  logdivlti  26941  logcnlem4  26966  logf1o2  26971  cxpcn3lem  27068  cxpaddle  27073  ang180lem2  27131  atanlogsublem  27236  atantan  27244  atanbndlem  27246  atans2  27252  leibpi  27263  log2tlbnd  27266  birthdaylem3  27274  efrlim  27290  jensenlem2  27308  zetacvg  27335  ftalem1  27393  ftalem5  27397  basellem1  27401  basellem4  27404  fsumdvdsdiaglem  27503  dvdsflf1o  27507  fsumfldivdiaglem  27509  ppiub  27524  mersenne  27547  dchrptlem1  27584  bposlem1  27604  bposlem2  27605  bposlem4  27607  lgsdilem  27644  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgsquadlem1  27700  lgsquadlem2  27701  2sqlem3  27740  2sqlem8  27746  2sqlem11  27749  2sqblem  27751  chebbnd1lem2  27790  chebbnd1lem3  27791  rplogsumlem1  27804  rplogsumlem2  27805  dchrisumlem1  27809  dchrmusum2  27814  dchrisum0flblem1  27828  mulog2sumlem1  27854  logdivbnd  27876  pntpbnd1a  27905  pntpbnd1  27906  pntpbnd2  27907  pntlemh  27919  pntlemr  27922  pntlemk  27926  pntlemo  27927  ostth2lem1  27938  ostth2lem2  27954  ostth2lem3  27955  ostth3  27958  noextenddif  28018  noextendlt  28019  noextendgt  28020  nosupbnd1lem3  28060  nosupbnd1lem4  28061  nosupbnd1lem5  28062  nosupbnd1lem6  28063  noinfbnd1lem3  28075  noinfbnd1lem4  28076  noinfbnd1lem5  28077  noinfbnd1lem6  28078  noetasuplem4  28086  madecut  28262  cofcut2  28301  eucliddivs  28755  legov  29041  axsegcon  29498  axpaschlem  29511  0uhgrsubgr  29853  clwwlkf1  30633  upgr4cycl4dv4e  30779  eupth2lem3lem3  30824  nrt2irr  31067  nmblolbii  31394  nmbdoplbi  32619  nmcoplbi  32623  nmophmi  32626  nmbdfnlbi  32644  nmcfnlbi  32647  cnlnadjlem7  32668  nmopcoi  32690  resf1o  33315  receqid  33329  xdivrec  33486  cycpmfvlem  33666  cycpmfv3  33669  lbsdiflsp0  34251  txomap  34459  unitdivcld  34526  measvunilem  34838  measvuni  34840  measssd  34841  measiuns  34843  measinblem  34846  measdivcst  34850  sibfof  34965  oddpwdc  34979  sseqfv1  35014  sseqfv2  35019  probun  35044  totprobd  35051  dstrvprob  35097  actfunsnrndisj  35227  reprsuc  35237  breprexplema  35252  subfaclim  35932  connpconn  35979  cvmliftlem2  36030  cvmliftlem6  36034  cvmliftlem7  36035  cvmliftlem8  36036  cvmliftlem9  36037  cvmliftlem10  36038  snmlff  36073  lineext  36821  hilbert1.1  36899  nn0prpwlem  37090  poimirlem1  38519  opnmbllem0  38554  ismblfin  38559  itgabsnc  38587  ftc1cnnclem  38589  bfplem1  38736  bfp  38738  lfl1  40107  lfladdcl  40108  eqlkr  40136  lkrlsp  40139  atcvrj2b  40469  3dim1  40504  3dim2  40505  llni2  40549  2llnjaN  40603  lvoli3  40614  lvoli2  40618  lncvrelatN  40818  lhpat4N  41081  lhpat3  41083  4atexlemex6  41111  ldilco  41153  ltrnid  41172  ltrnatb  41174  ltrnel  41176  ltrncnvel  41179  ltrncnv  41183  ltrn11at  41184  ltrneq  41186  trlat  41206  trlator0  41208  ltrnnidn  41211  trlid0  41213  trlnidatb  41214  trlnle  41223  trlval3  41224  trlval4  41225  cdlemc2  41229  cdlemc5  41232  cdlemc6  41233  cdlemc  41234  cdlemd2  41236  cdlemd9  41243  cdleme0e  41254  cdleme02N  41259  cdleme0ex1N  41260  cdleme3e  41269  cdleme3g  41271  cdleme3h  41272  cdleme3  41274  cdleme7aa  41279  cdleme7b  41281  cdleme7c  41282  cdleme7d  41283  cdleme7e  41284  cdleme7ga  41285  cdleme7  41286  cdleme9  41290  cdleme16aN  41296  cdleme11c  41298  cdleme11dN  41299  cdleme11e  41300  cdleme11h  41303  cdleme11j  41304  cdleme11k  41305  cdleme12  41308  cdleme21j  41373  cdleme26eALTN  41398  cdleme26f  41400  cdleme26f2  41402  cdlemefrs29bpre0  41433  cdleme35a  41485  cdleme35b  41487  cdleme35c  41488  cdleme35f  41491  cdleme36a  41497  cdleme38m  41500  cdlemeg46rgv  41565  cdlemeg46req  41566  cdlemf  41600  cdlemg2fvlem  41631  cdlemg2l  41640  cdlemg7N  41663  cdlemg12g  41686  cdlemg15  41693  cdlemg17h  41705  cdlemg17  41714  cdlemg19a  41720  cdlemg24  41725  cdlemg37  41726  cdlemg27a  41729  cdlemg31b0N  41731  cdlemg27b  41733  cdlemg31c  41736  cdlemg31d  41737  cdlemg35  41750  trljco  41777  tgrpgrplem  41786  cdlemh2  41853  tendoconid  41866  tendotr  41867  cdlemk35s-id  41975  cdlemk39s-id  41977  cdlemk53b  41993  cdlemk53  41994  cdlemk54  41995  cdleml3N  42015  cdleml5N  42017  tendospcanN  42060  diclss  42230  dihvalcq2  42284  dihord4  42295  dihord5b  42296  dihord5apre  42299  dihmeetlem1N  42327  dihmeetbclemN  42341  dihmeetlem20N  42363  dihmeetALTN  42364  dihatlat  42371  dihatexv  42375  dochkr1  42515  dochkr1OLDN  42516  lcfl7lem  42536  lclkrlem2m  42556  hdmaplna1  42944  hdmaplns1  42945  hdmaplnm1  42946  cxp111d  43373  eldioph2lem1  43750  fphpdo  43803  irrapxlem1  43808  irrapxlem2  43809  irrapxlem3  43810  irrapxlem5  43812  pellexlem2  43816  pell1234qrreccl  43840  pell1234qrmulcl  43841  pell1234qrdich  43847  pell1qr1  43857  pellqrexplicit  43863  pellfundex  43872  reglogltb  43877  reglogleb  43878  pellfund14  43884  rmxycomplete  43903  jm2.24nn  43945  jm2.17b  43947  jm2.17c  43948  jm2.18  43974  jm2.19lem2  43976  jm2.20nn  43983  jm2.16nn0  43990  jm3.1lem2  44004  areaquad  44202  clsk3nimkb  45025  lemuldiv3d  45155  lemuldiv4d  45156  stoweidlem1  46980  stoweidlem11  46990  stoweidlem14  46993  stoweidlem26  47005  stoweidlem34  47013  stoweidlem38  47017  stoweidlem60  47039  fourierdlem52  47137  etransclem38  47251  2tceilhalfelfzo1  48375  reuopreuprim  48577  nprmdvdsfacm1lem4  48677  quad1  48687  requad1  48689  requad2  48690  isubgr3stgrlem1  49033  isubgr3stgrlem3  49035  gpg3kgrtriexlem1  49150  gpg3kgrtriexlem5  49154  domnmsuppn0  49450  lincvalpr  49499  ldepspr  49554  islindeps2  49564  fldivexpfllog2  49646  eenglngeehlnmlem1  49818  eenglngeehlnmlem2  49819  rrx2linest  49823  prsthinc  50541