Theorem syl112anc 1402

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 1399	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  3844  2nreu  4405  fveqf1o  7341  frrlem12  8353  enfixsn  9143  gruina  10942  grur1  10944  enqeq  11058  muldivdid  12051  recrec  12054  rec11r  12056  divdivdiv  12058  dmdcan  12067  ddcan  12071  rereccl  12075  div2neg  12080  divmuld  12155  divmul2d  12166  divmul3d  12167  divassd  12168  div12d  12169  div23d  12170  divdird  12171  divsubdird  12172  div11d  12173  ltmul12a  12213  ltdiv1  12221  ltrec  12239  lt2msq1  12241  lediv2  12247  supmul1  12326  qbtwnre  13369  xlemul1a  13458  xlemul1  13460  xadd4d  13473  quoremz  14035  quoremnn0ALT  14037  expgt1  14283  nnlesq  14389  expnbnd  14417  expmulnbnd  14420  discr1  14424  facubnd  14485  pfxsuffeqwrdeq  14889  01sqrexlem6  15457  mulcn2  15807  geomulcvg  16089  cvgrat  16096  eftlub  16321  eflegeo  16333  tanhlt1  16372  sin01bnd  16397  cos01bnd  16398  eirrlem  16416  bitsmod  16650  mulgcd  16765  mulgcddvds  16874  prmind2  16904  qnumgt0  16970  pcpremul  17065  fldivp1  17119  pcfaclem  17120  qexpz  17123  prmpwdvds  17126  pockthg  17128  prmreclem1  17138  prmreclem5  17142  4sqlem10  17169  4sqlem12  17178  4sqlem16  17182  4sqlem17  17183  vdwlem3  17205  vdwlem8  17210  vdwlem9  17211  0ram  17242  ramz2  17246  cat1lem  18321  odmulg  19821  dfod2  19829  odf1o1  19837  odf1o2  19838  sylow3lem4  19895  ablsub4  20075  odadd1  20113  odadd2  20114  ablfacrp2  20334  ablfac1b  20337  ablfac1eu  20340  pgpfac1lem3a  20343  pgpfaclem2  20349  ablsimpgfindlem1  20374  chrcong  21888  znrrg  21926  cygznlem1  21927  chpdmatlem3  23213  txdis  24006  txdis1cn  24009  ptunhmeo  24182  qustgplem  24495  blcld  24879  nlmvscnlem2  25059  blcvx  25172  metds0  25225  metdseq0  25229  icopnfcnv  25318  lebnumii  25342  ipcau2  25610  tcphcphlem1  25611  ipcnlem2  25620  csbren  25775  trirn  25776  dyadf  25967  dyadovol  25969  dyaddisjlem  25971  dyadmaxlem  25973  opnmbllem  25977  mbfmulc2lem  26023  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  itg2mulclem  26122  itg2monolem1  26126  itg2monolem3  26128  itg2cnlem2  26138  itgabs  26210  dvlip  26368  dvlt0  26380  dvcvx  26395  ftc1lem4  26414  dgrcolem2  26648  aaliou3lem2  26727  aaliou3lem9  26734  itgulm  26792  radcnvlem1  26797  abelthlem2  26816  abelthlem7  26822  tangtx  26891  cosne0  26914  cosordlem  26915  tanord1  26922  logdivlti  27005  logcnlem4  27030  logf1o2  27035  cxpcn3lem  27132  cxpaddle  27137  ang180lem2  27195  atanlogsublem  27300  atantan  27308  atanbndlem  27310  atans2  27316  leibpi  27327  log2tlbnd  27330  birthdaylem3  27338  efrlim  27354  jensenlem2  27372  zetacvg  27399  ftalem1  27457  ftalem5  27461  basellem1  27465  basellem4  27468  fsumdvdsdiaglem  27567  dvdsflf1o  27571  fsumfldivdiaglem  27573  ppiub  27588  mersenne  27611  dchrptlem1  27648  bposlem1  27668  bposlem2  27669  bposlem4  27671  lgsdilem  27708  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgsquadlem1  27764  lgsquadlem2  27765  2sqlem3  27804  2sqlem8  27810  2sqlem11  27813  2sqblem  27815  chebbnd1lem2  27854  chebbnd1lem3  27855  rplogsumlem1  27868  rplogsumlem2  27869  dchrisumlem1  27873  dchrmusum2  27878  dchrisum0flblem1  27892  mulog2sumlem1  27918  logdivbnd  27940  pntpbnd1a  27969  pntpbnd1  27970  pntpbnd2  27971  pntlemh  27983  pntlemr  27986  pntlemk  27990  pntlemo  27991  ostth2lem1  28002  ostth2lem2  28018  ostth2lem3  28019  ostth3  28022  noextenddif  28082  noextendlt  28083  noextendgt  28084  nosupbnd1lem3  28124  nosupbnd1lem4  28125  nosupbnd1lem5  28126  nosupbnd1lem6  28127  noinfbnd1lem3  28139  noinfbnd1lem4  28140  noinfbnd1lem5  28141  noinfbnd1lem6  28142  noetasuplem4  28150  madecut  28326  cofcut2  28365  eucliddivs  28819  legov  29105  axsegcon  29562  axpaschlem  29575  0uhgrsubgr  29917  clwwlkf1  30697  upgr4cycl4dv4e  30843  eupth2lem3lem3  30888  nrt2irr  31131  nmblolbii  31458  nmbdoplbi  32683  nmcoplbi  32687  nmophmi  32690  nmbdfnlbi  32708  nmcfnlbi  32711  cnlnadjlem7  32732  nmopcoi  32754  resf1o  33418  receqid  33432  xdivrec  33589  cycpmfvlem  33772  cycpmfv3  33775  lbsdiflsp0  34369  txomap  34577  unitdivcld  34644  measvunilem  34956  measvuni  34958  measssd  34959  measiuns  34961  measinblem  34964  measdivcst  34968  sibfof  35083  oddpwdc  35097  sseqfv1  35132  sseqfv2  35137  probun  35162  totprobd  35169  dstrvprob  35215  actfunsnrndisj  35345  reprsuc  35355  breprexplema  35370  subfaclim  36161  connpconn  36208  cvmliftlem2  36259  cvmliftlem6  36263  cvmliftlem7  36264  cvmliftlem8  36265  cvmliftlem9  36266  cvmliftlem10  36267  snmlff  36302  lineext  37056  hilbert1.1  37134  nn0prpwlem  37325  poimirlem1  38807  opnmbllem0  38842  ismblfin  38847  itgabsnc  38875  ftc1cnnclem  38877  bfplem1  39022  bfp  39024  lfl1  40393  lfladdcl  40394  eqlkr  40422  lkrlsp  40425  atcvrj2b  40755  3dim1  40790  3dim2  40791  llni2  40835  2llnjaN  40889  lvoli3  40900  lvoli2  40904  lncvrelatN  41104  lhpat4N  41367  lhpat3  41369  4atexlemex6  41397  ldilco  41439  ltrnid  41458  ltrnatb  41460  ltrnel  41462  ltrncnvel  41465  ltrncnv  41469  ltrn11at  41470  ltrneq  41472  trlat  41492  trlator0  41494  ltrnnidn  41497  trlid0  41499  trlnidatb  41500  trlnle  41509  trlval3  41510  trlval4  41511  cdlemc2  41515  cdlemc5  41518  cdlemc6  41519  cdlemc  41520  cdlemd2  41522  cdlemd9  41529  cdleme0e  41540  cdleme02N  41545  cdleme0ex1N  41546  cdleme3e  41555  cdleme3g  41557  cdleme3h  41558  cdleme3  41560  cdleme7aa  41565  cdleme7b  41567  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme7ga  41571  cdleme7  41572  cdleme9  41576  cdleme16aN  41582  cdleme11c  41584  cdleme11dN  41585  cdleme11e  41586  cdleme11h  41589  cdleme11j  41590  cdleme11k  41591  cdleme12  41594  cdleme21j  41659  cdleme26eALTN  41684  cdleme26f  41686  cdleme26f2  41688  cdlemefrs29bpre0  41719  cdleme35a  41771  cdleme35b  41773  cdleme35c  41774  cdleme35f  41777  cdleme36a  41783  cdleme38m  41786  cdlemeg46rgv  41851  cdlemeg46req  41852  cdlemf  41886  cdlemg2fvlem  41917  cdlemg2l  41926  cdlemg7N  41949  cdlemg12g  41972  cdlemg15  41979  cdlemg17h  41991  cdlemg17  42000  cdlemg19a  42006  cdlemg24  42011  cdlemg37  42012  cdlemg27a  42015  cdlemg31b0N  42017  cdlemg27b  42019  cdlemg31c  42022  cdlemg31d  42023  cdlemg35  42036  trljco  42063  tgrpgrplem  42072  cdlemh2  42139  tendoconid  42152  tendotr  42153  cdlemk35s-id  42261  cdlemk39s-id  42263  cdlemk53b  42279  cdlemk53  42280  cdlemk54  42281  cdleml3N  42301  cdleml5N  42303  tendospcanN  42346  diclss  42516  dihvalcq2  42570  dihord4  42581  dihord5b  42582  dihord5apre  42585  dihmeetlem1N  42613  dihmeetbclemN  42627  dihmeetlem20N  42649  dihmeetALTN  42650  dihatlat  42657  dihatexv  42661  dochkr1  42801  dochkr1OLDN  42802  lcfl7lem  42822  lclkrlem2m  42842  hdmaplna1  43230  hdmaplns1  43231  hdmaplnm1  43232  cxp111d  43659  eldioph2lem1  44037  fphpdo  44090  irrapxlem1  44095  irrapxlem2  44096  irrapxlem3  44097  irrapxlem5  44099  pellexlem2  44103  pell1234qrreccl  44127  pell1234qrmulcl  44128  pell1234qrdich  44134  pell1qr1  44144  pellqrexplicit  44150  pellfundex  44159  reglogltb  44164  reglogleb  44165  pellfund14  44171  rmxycomplete  44190  jm2.24nn  44232  jm2.17b  44234  jm2.17c  44235  jm2.18  44261  jm2.19lem2  44263  jm2.20nn  44270  jm2.16nn0  44277  jm3.1lem2  44291  areaquad  44479  clsk3nimkb  45301  lemuldiv3d  45431  lemuldiv4d  45432  stoweidlem1  47284  stoweidlem11  47294  stoweidlem14  47297  stoweidlem26  47309  stoweidlem34  47317  stoweidlem38  47321  stoweidlem60  47343  fourierdlem52  47441  etransclem38  47555  2tceilhalfelfzo1  48679  reuopreuprim  48881  nprmdvdsfacm1lem4  48981  quad1  48991  requad1  48993  requad2  48994  isubgr3stgrlem1  49337  isubgr3stgrlem3  49339  gpg3kgrtriexlem1  49454  gpg3kgrtriexlem5  49458  domnmsuppn0  49812  lincvalpr  49861  ldepspr  49916  islindeps2  49926  fldivexpfllog2  50008  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  rrx2linest  50185  prsthinc  50930