Theorem syl22anc 1251

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 1248	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  5573  tfrexlem  6427  th3qlem1  6731  en2prd  6916  enpr2d  6918  ssenen  6955  phplem4dom  6966  phplem4on  6971  fiunsnnn  6985  findcard2sd  6996  unsnfi  7023  sbthlemi9  7074  endjusym  7205  endjudisj  7329  djuen  7330  ltanqg  7520  ltmnqg  7521  ltnnnq  7543  addcmpblnq0  7563  addlocprlemeqgt  7652  distrlem1prl  7702  distrlem1pru  7703  distrlem4prl  7704  distrlem4pru  7705  addcanprleml  7734  recexprlem1ssl  7753  caucvgprlemloc  7795  caucvgprprlemloccalc  7804  mulcmpblnr  7861  ltasrg  7890  recexgt0sr  7893  mulextsr1lem  7900  mulextsr1  7901  srpospr  7903  prsrlt  7907  ltpsrprg  7923  mappsrprg  7924  pitonnlem1p1  7966  recidpirq  7978  axpre-ltadd  8006  mulgt0d  8202  mul4d  8234  add4d  8248  add42d  8249  subcan  8334  addsub4d  8437  subadd4d  8438  sub4d  8439  2addsubd  8440  addsubeq4d  8441  muladdd  8495  mulsubd  8496  addgegt0d  8599  addgtge0d  8600  addge0d  8602  le2addd  8643  le2subd  8644  ltleaddd  8645  leltaddd  8646  lt2subd  8648  apreap  8667  apsym  8686  apcotr  8687  apadd1  8688  apneg  8691  mulext1  8692  mulap0r  8695  mulge0d  8701  mulap0d  8738  divdivdivap  8793  divcanap5  8794  divap0d  8886  recdivapd  8887  recdivap2d  8888  divcanap6d  8889  ddcanapd  8890  rec11apd  8891  divmuldivapd  8912  divmuleqapd  8913  subrecapd  8921  prodgt0  8932  lt2msq  8966  ledivdiv  8970  lediv12a  8974  recreclt  8980  divgt0d  9015  mulgt1d  9016  lemulge11d  9017  lemulge12d  9018  ltmul12ad  9021  lemul12ad  9022  lemul12bd  9023  nndivtr  9085  qreccl  9770  ledivdivd  9851  lediv12ad  9885  lt2mul2divd  9894  xlt2add  10009  xleaddadd  10016  iccss2  10073  iccssico2  10076  lincmb01cmp  10132  iccf1o  10133  fzrev2i  10215  qtri3or  10390  elicore  10416  2tnp1ge0ge0  10451  modqid  10501  q0mod  10507  q1mod  10508  modqabs  10509  modqadd1  10513  mulqaddmodid  10516  mulp1mod1  10517  modqmuladd  10518  modqmuladdnn0  10520  qnegmod  10521  m1modnnsub1  10522  addmodid  10524  modqm1p1mod0  10527  modqltm1p1mod  10528  modqmul1  10529  q2submod  10537  modifeq2int  10538  modaddmodup  10539  modaddmodlo  10540  modqaddmulmod  10543  modqsubdir  10545  modqeqmodmin  10546  modsumfzodifsn  10548  addmodlteq  10550  frecfzennn  10578  ser3mono  10639  expcl2lemap  10703  mulexpzap  10731  expaddzaplem  10734  expaddzap  10735  expmulzap  10737  ltexp2a  10743  leexp2a  10744  sqdivap  10755  qsqeqor  10802  expnbnd  10815  expsubapd  10836  lt2sqd  10856  le2sqd  10857  sq11d  10858  apexp1  10870  bcp1nk  10914  hashunlem  10956  zfz1isolem1  10992  cjap  11261  cnreim  11333  resqrexlem1arp  11360  resqrexlemp1rp  11361  resqrexlemglsq  11377  abs00ap  11417  absext  11418  absexpzap  11435  absrele  11438  sqrtmuld  11524  sqrtsq2d  11525  sqrtled  11526  sqrtltd  11527  sqr11d  11528  abs3lemd  11556  minmax  11585  xrmaxiflemlub  11603  xrltmaxsup  11612  xrminmax  11620  xrbdtri  11631  climuni  11648  2clim  11656  addcn2  11665  mulcn2  11667  fsum3  11742  mptfzshft  11797  fsumrev  11798  fisum0diag2  11802  modfsummodlemstep  11812  binomlem  11838  mertenslemi1  11890  fprodrev  11974  efcllemp  12013  p1modz1  12149  dvds1  12208  dvdsext  12210  mulmoddvds  12218  oexpneg  12232  evennn02n  12237  evennn2n  12238  bitsinv1  12317  bezoutlemmo  12371  mulgcd  12381  dvdssqlem  12395  rpmulgcd2  12461  isprm6  12513  sqrt2irraplemnn  12545  sqrt2irrap  12546  crth  12590  eulerthlemh  12597  prmdiveq  12602  powm2modprm  12619  modprm0  12621  pythagtriplem2  12633  pythagtriplem11  12641  pythagtriplem13  12643  pythagtrip  12650  pcid  12691  pcgcd1  12695  pcprmpw2  12700  dvdsprmpweqle  12704  pcaddlem  12706  pcadd  12707  fldivp1  12715  4sqlem12  12769  4sqlem14  12771  4sqlem15  12772  4sqlem16  12773  unennn  12812  ennnfonelemg  12818  ennnfonelemhf1o  12828  inffinp1  12844  isstructr  12891  setscomd  12917  imasbas  13183  imasplusg  13184  imasmulr  13185  subm0  13358  lssvancl1  14173  lssvnegcl  14182  lspprvacl  14219  lspsneli  14221  lspsn  14222  znf1o  14457  ntrin  14640  topssnei  14678  restbasg  14684  cnntri  14740  txcn  14791  txlm  14795  cnmpt2res  14813  psmetlecl  14850  xmetlecl  14883  bldisj  14917  bdmet  15018  bdbl  15019  bdmopn  15020  xmetxp  15023  metcnp  15028  tgioo  15070  cncfmet  15108  dedekindeulemlub  15136  suplociccreex  15140  ellimc3apf  15176  limcimolemlt  15180  limccnp2cntop  15193  dvfvalap  15197  dvidsslem  15209  dvmulxxbr  15218  dvaddxx  15219  dvmulxx  15220  dviaddf  15221  dvimulf  15222  dvcoapbr  15223  dvmptclx  15234  cxplt3  15436  cxpltd  15444  cxpled  15445  cxplt3d  15451  cxple3d  15452  logbrec  15476  logbgcd1irraplemap  15485  wilthlem1  15496  mpodvdsmulf1o  15506  lgslem1  15521  lgslem3  15523  lgsdirprm  15555  gausslemma2dlem1f1o  15581  gausslemma2dlem6  15588  lgseisenlem1  15591  lgseisenlem2  15592  lgseisenlem4  15594  lgseisen  15595  lgsquadlem1  15598  lgsquad2lem1  15602  lgsquad3  15605  m1lgs  15606  2lgslem1a1  15607  2sqlem7  15642