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  5622  tfrexlem  6491  th3qlem1  6797  en2prd  6983  enpr2d  6985  ssenen  7025  phplem4dom  7036  phplem4on  7042  fiunsnnn  7056  findcard2sd  7067  unsnfi  7097  sbthlemi9  7148  endjusym  7279  endjudisj  7408  djuen  7409  ltanqg  7603  ltmnqg  7604  ltnnnq  7626  addcmpblnq0  7646  addlocprlemeqgt  7735  distrlem1prl  7785  distrlem1pru  7786  distrlem4prl  7787  distrlem4pru  7788  addcanprleml  7817  recexprlem1ssl  7836  caucvgprlemloc  7878  caucvgprprlemloccalc  7887  mulcmpblnr  7944  ltasrg  7973  recexgt0sr  7976  mulextsr1lem  7983  mulextsr1  7984  srpospr  7986  prsrlt  7990  ltpsrprg  8006  mappsrprg  8007  pitonnlem1p1  8049  recidpirq  8061  axpre-ltadd  8089  mulgt0d  8285  mul4d  8317  add4d  8331  add42d  8332  subcan  8417  addsub4d  8520  subadd4d  8521  sub4d  8522  2addsubd  8523  addsubeq4d  8524  muladdd  8578  mulsubd  8579  addgegt0d  8682  addgtge0d  8683  addge0d  8685  le2addd  8726  le2subd  8727  ltleaddd  8728  leltaddd  8729  lt2subd  8731  apreap  8750  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  mulap0r  8778  mulge0d  8784  mulap0d  8821  divdivdivap  8876  divcanap5  8877  divap0d  8969  recdivapd  8970  recdivap2d  8971  divcanap6d  8972  ddcanapd  8973  rec11apd  8974  divmuldivapd  8995  divmuleqapd  8996  subrecapd  9004  prodgt0  9015  lt2msq  9049  ledivdiv  9053  lediv12a  9057  recreclt  9063  divgt0d  9098  mulgt1d  9099  lemulge11d  9100  lemulge12d  9101  ltmul12ad  9104  lemul12ad  9105  lemul12bd  9106  nndivtr  9168  qreccl  9854  ledivdivd  9935  lediv12ad  9969  lt2mul2divd  9978  xlt2add  10093  xleaddadd  10100  iccss2  10157  iccssico2  10160  lincmb01cmp  10216  iccf1o  10217  fzrev2i  10299  qtri3or  10477  elicore  10503  2tnp1ge0ge0  10538  modqid  10588  q0mod  10594  q1mod  10595  modqabs  10596  modqadd1  10600  mulqaddmodid  10603  mulp1mod1  10604  modqmuladd  10605  modqmuladdnn0  10607  qnegmod  10608  m1modnnsub1  10609  addmodid  10611  modqm1p1mod0  10614  modqltm1p1mod  10615  modqmul1  10616  q2submod  10624  modifeq2int  10625  modaddmodup  10626  modaddmodlo  10627  modqaddmulmod  10630  modqsubdir  10632  modqeqmodmin  10633  modsumfzodifsn  10635  addmodlteq  10637  frecfzennn  10665  ser3mono  10726  expcl2lemap  10790  mulexpzap  10818  expaddzaplem  10821  expaddzap  10822  expmulzap  10824  ltexp2a  10830  leexp2a  10831  sqdivap  10842  qsqeqor  10889  expnbnd  10902  expsubapd  10923  lt2sqd  10943  le2sqd  10944  sq11d  10945  apexp1  10957  bcp1nk  11001  hashunlem  11043  zfz1isolem1  11080  cjap  11438  cnreim  11510  resqrexlem1arp  11537  resqrexlemp1rp  11538  resqrexlemglsq  11554  abs00ap  11594  absext  11595  absexpzap  11612  absrele  11615  sqrtmuld  11701  sqrtsq2d  11702  sqrtled  11703  sqrtltd  11704  sqr11d  11705  abs3lemd  11733  minmax  11762  xrmaxiflemlub  11780  xrltmaxsup  11789  xrminmax  11797  xrbdtri  11808  climuni  11825  2clim  11833  addcn2  11842  mulcn2  11844  fsum3  11919  mptfzshft  11974  fsumrev  11975  fisum0diag2  11979  modfsummodlemstep  11989  binomlem  12015  mertenslemi1  12067  fprodrev  12151  efcllemp  12190  p1modz1  12326  dvds1  12385  dvdsext  12387  mulmoddvds  12395  oexpneg  12409  evennn02n  12414  evennn2n  12415  bitsinv1  12494  bezoutlemmo  12548  mulgcd  12558  dvdssqlem  12572  rpmulgcd2  12638  isprm6  12690  sqrt2irraplemnn  12722  sqrt2irrap  12723  crth  12767  eulerthlemh  12774  prmdiveq  12779  powm2modprm  12796  modprm0  12798  pythagtriplem2  12810  pythagtriplem11  12818  pythagtriplem13  12820  pythagtrip  12827  pcid  12868  pcgcd1  12872  pcprmpw2  12877  dvdsprmpweqle  12881  pcaddlem  12883  pcadd  12884  fldivp1  12892  4sqlem12  12946  4sqlem14  12948  4sqlem15  12949  4sqlem16  12950  unennn  12989  ennnfonelemg  12995  ennnfonelemhf1o  13005  inffinp1  13021  isstructr  13068  setscomd  13094  imasbas  13361  imasplusg  13362  imasmulr  13363  subm0  13536  lssvancl1  14352  lssvnegcl  14361  lspprvacl  14398  lspsneli  14400  lspsn  14401  znf1o  14636  ntrin  14819  topssnei  14857  restbasg  14863  cnntri  14919  txcn  14970  txlm  14974  cnmpt2res  14992  psmetlecl  15029  xmetlecl  15062  bldisj  15096  bdmet  15197  bdbl  15198  bdmopn  15199  xmetxp  15202  metcnp  15207  tgioo  15249  cncfmet  15287  dedekindeulemlub  15315  suplociccreex  15319  ellimc3apf  15355  limcimolemlt  15359  limccnp2cntop  15372  dvfvalap  15376  dvidsslem  15388  dvmulxxbr  15397  dvaddxx  15398  dvmulxx  15399  dviaddf  15400  dvimulf  15401  dvcoapbr  15402  dvmptclx  15413  cxplt3  15615  cxpltd  15623  cxpled  15624  cxplt3d  15630  cxple3d  15631  logbrec  15655  logbgcd1irraplemap  15664  wilthlem1  15675  mpodvdsmulf1o  15685  lgslem1  15700  lgslem3  15702  lgsdirprm  15734  gausslemma2dlem1f1o  15760  gausslemma2dlem6  15767  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem4  15773  lgseisen  15774  lgsquadlem1  15777  lgsquad2lem1  15781  lgsquad3  15784  m1lgs  15785  2lgslem1a1  15786  2sqlem7  15821  usgredg2v  16043  vtxd0nedgbfi  16085