Theorem syl22anc 1272

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

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl22anc.5	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl22anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 306	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylXanc.3	. 2 ⊢ (𝜑 → 𝜃)
5		sylXanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 1269	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  f1oprg  5619  tfrexlem  6486  th3qlem1  6792  en2prd  6978  enpr2d  6980  ssenen  7020  phplem4dom  7031  phplem4on  7037  fiunsnnn  7051  findcard2sd  7062  unsnfi  7089  sbthlemi9  7140  endjusym  7271  endjudisj  7400  djuen  7401  ltanqg  7595  ltmnqg  7596  ltnnnq  7618  addcmpblnq0  7638  addlocprlemeqgt  7727  distrlem1prl  7777  distrlem1pru  7778  distrlem4prl  7779  distrlem4pru  7780  addcanprleml  7809  recexprlem1ssl  7828  caucvgprlemloc  7870  caucvgprprlemloccalc  7879  mulcmpblnr  7936  ltasrg  7965  recexgt0sr  7968  mulextsr1lem  7975  mulextsr1  7976  srpospr  7978  prsrlt  7982  ltpsrprg  7998  mappsrprg  7999  pitonnlem1p1  8041  recidpirq  8053  axpre-ltadd  8081  mulgt0d  8277  mul4d  8309  add4d  8323  add42d  8324  subcan  8409  addsub4d  8512  subadd4d  8513  sub4d  8514  2addsubd  8515  addsubeq4d  8516  muladdd  8570  mulsubd  8571  addgegt0d  8674  addgtge0d  8675  addge0d  8677  le2addd  8718  le2subd  8719  ltleaddd  8720  leltaddd  8721  lt2subd  8723  apreap  8742  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  mulap0r  8770  mulge0d  8776  mulap0d  8813  divdivdivap  8868  divcanap5  8869  divap0d  8961  recdivapd  8962  recdivap2d  8963  divcanap6d  8964  ddcanapd  8965  rec11apd  8966  divmuldivapd  8987  divmuleqapd  8988  subrecapd  8996  prodgt0  9007  lt2msq  9041  ledivdiv  9045  lediv12a  9049  recreclt  9055  divgt0d  9090  mulgt1d  9091  lemulge11d  9092  lemulge12d  9093  ltmul12ad  9096  lemul12ad  9097  lemul12bd  9098  nndivtr  9160  qreccl  9845  ledivdivd  9926  lediv12ad  9960  lt2mul2divd  9969  xlt2add  10084  xleaddadd  10091  iccss2  10148  iccssico2  10151  lincmb01cmp  10207  iccf1o  10208  fzrev2i  10290  qtri3or  10468  elicore  10494  2tnp1ge0ge0  10529  modqid  10579  q0mod  10585  q1mod  10586  modqabs  10587  modqadd1  10591  mulqaddmodid  10594  mulp1mod1  10595  modqmuladd  10596  modqmuladdnn0  10598  qnegmod  10599  m1modnnsub1  10600  addmodid  10602  modqm1p1mod0  10605  modqltm1p1mod  10606  modqmul1  10607  q2submod  10615  modifeq2int  10616  modaddmodup  10617  modaddmodlo  10618  modqaddmulmod  10621  modqsubdir  10623  modqeqmodmin  10624  modsumfzodifsn  10626  addmodlteq  10628  frecfzennn  10656  ser3mono  10717  expcl2lemap  10781  mulexpzap  10809  expaddzaplem  10812  expaddzap  10813  expmulzap  10815  ltexp2a  10821  leexp2a  10822  sqdivap  10833  qsqeqor  10880  expnbnd  10893  expsubapd  10914  lt2sqd  10934  le2sqd  10935  sq11d  10936  apexp1  10948  bcp1nk  10992  hashunlem  11034  zfz1isolem1  11070  cjap  11425  cnreim  11497  resqrexlem1arp  11524  resqrexlemp1rp  11525  resqrexlemglsq  11541  abs00ap  11581  absext  11582  absexpzap  11599  absrele  11602  sqrtmuld  11688  sqrtsq2d  11689  sqrtled  11690  sqrtltd  11691  sqr11d  11692  abs3lemd  11720  minmax  11749  xrmaxiflemlub  11767  xrltmaxsup  11776  xrminmax  11784  xrbdtri  11795  climuni  11812  2clim  11820  addcn2  11829  mulcn2  11831  fsum3  11906  mptfzshft  11961  fsumrev  11962  fisum0diag2  11966  modfsummodlemstep  11976  binomlem  12002  mertenslemi1  12054  fprodrev  12138  efcllemp  12177  p1modz1  12313  dvds1  12372  dvdsext  12374  mulmoddvds  12382  oexpneg  12396  evennn02n  12401  evennn2n  12402  bitsinv1  12481  bezoutlemmo  12535  mulgcd  12545  dvdssqlem  12559  rpmulgcd2  12625  isprm6  12677  sqrt2irraplemnn  12709  sqrt2irrap  12710  crth  12754  eulerthlemh  12761  prmdiveq  12766  powm2modprm  12783  modprm0  12785  pythagtriplem2  12797  pythagtriplem11  12805  pythagtriplem13  12807  pythagtrip  12814  pcid  12855  pcgcd1  12859  pcprmpw2  12864  dvdsprmpweqle  12868  pcaddlem  12870  pcadd  12871  fldivp1  12879  4sqlem12  12933  4sqlem14  12935  4sqlem15  12936  4sqlem16  12937  unennn  12976  ennnfonelemg  12982  ennnfonelemhf1o  12992  inffinp1  13008  isstructr  13055  setscomd  13081  imasbas  13348  imasplusg  13349  imasmulr  13350  subm0  13523  lssvancl1  14339  lssvnegcl  14348  lspprvacl  14385  lspsneli  14387  lspsn  14388  znf1o  14623  ntrin  14806  topssnei  14844  restbasg  14850  cnntri  14906  txcn  14957  txlm  14961  cnmpt2res  14979  psmetlecl  15016  xmetlecl  15049  bldisj  15083  bdmet  15184  bdbl  15185  bdmopn  15186  xmetxp  15189  metcnp  15194  tgioo  15236  cncfmet  15274  dedekindeulemlub  15302  suplociccreex  15306  ellimc3apf  15342  limcimolemlt  15346  limccnp2cntop  15359  dvfvalap  15363  dvidsslem  15375  dvmulxxbr  15384  dvaddxx  15385  dvmulxx  15386  dviaddf  15387  dvimulf  15388  dvcoapbr  15389  dvmptclx  15400  cxplt3  15602  cxpltd  15610  cxpled  15611  cxplt3d  15617  cxple3d  15618  logbrec  15642  logbgcd1irraplemap  15651  wilthlem1  15662  mpodvdsmulf1o  15672  lgslem1  15687  lgslem3  15689  lgsdirprm  15721  gausslemma2dlem1f1o  15747  gausslemma2dlem6  15754  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem4  15760  lgseisen  15761  lgsquadlem1  15764  lgsquad2lem1  15768  lgsquad3  15771  m1lgs  15772  2lgslem1a1  15773  2sqlem7  15808  usgredg2v  16030