Theorem syl22anc 1234

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 304	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylXanc.3	. 2 ⊢ (𝜑 → 𝜃)
5		sylXanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 1231	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  f1oprg  5486  tfrexlem  6313  th3qlem1  6615  enpr2d  6795  ssenen  6829  phplem4dom  6840  phplem4on  6845  fiunsnnn  6859  findcard2sd  6870  unsnfi  6896  sbthlemi9  6942  endjusym  7073  endjudisj  7187  djuen  7188  ltanqg  7362  ltmnqg  7363  ltnnnq  7385  addcmpblnq0  7405  addlocprlemeqgt  7494  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  addcanprleml  7576  recexprlem1ssl  7595  caucvgprlemloc  7637  caucvgprprlemloccalc  7646  mulcmpblnr  7703  ltasrg  7732  recexgt0sr  7735  mulextsr1lem  7742  mulextsr1  7743  srpospr  7745  prsrlt  7749  ltpsrprg  7765  mappsrprg  7766  pitonnlem1p1  7808  recidpirq  7820  axpre-ltadd  7848  mulgt0d  8042  mul4d  8074  add4d  8088  add42d  8089  subcan  8174  addsub4d  8277  subadd4d  8278  sub4d  8279  2addsubd  8280  addsubeq4d  8281  muladdd  8335  mulsubd  8336  addgegt0d  8438  addgtge0d  8439  addge0d  8441  le2addd  8482  le2subd  8483  ltleaddd  8484  leltaddd  8485  lt2subd  8487  apreap  8506  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  mulap0r  8534  mulge0d  8540  mulap0d  8576  divdivdivap  8630  divcanap5  8631  divap0d  8723  recdivapd  8724  recdivap2d  8725  divcanap6d  8726  ddcanapd  8727  rec11apd  8728  divmuldivapd  8749  divmuleqapd  8750  subrecapd  8758  prodgt0  8768  lt2msq  8802  ledivdiv  8806  lediv12a  8810  recreclt  8816  divgt0d  8851  mulgt1d  8852  lemulge11d  8853  lemulge12d  8854  ltmul12ad  8857  lemul12ad  8858  lemul12bd  8859  nndivtr  8920  qreccl  9601  ledivdivd  9679  lediv12ad  9713  lt2mul2divd  9722  xlt2add  9837  xleaddadd  9844  iccss2  9901  iccssico2  9904  lincmb01cmp  9960  iccf1o  9961  fzrev2i  10042  qtri3or  10199  elicore  10223  2tnp1ge0ge0  10257  modqid  10305  q0mod  10311  q1mod  10312  modqabs  10313  modqadd1  10317  mulqaddmodid  10320  mulp1mod1  10321  modqmuladd  10322  modqmuladdnn0  10324  qnegmod  10325  m1modnnsub1  10326  addmodid  10328  modqm1p1mod0  10331  modqltm1p1mod  10332  modqmul1  10333  q2submod  10341  modifeq2int  10342  modaddmodup  10343  modaddmodlo  10344  modqaddmulmod  10347  modqsubdir  10349  modqeqmodmin  10350  modsumfzodifsn  10352  addmodlteq  10354  frecfzennn  10382  ser3mono  10434  expcl2lemap  10488  mulexpzap  10516  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  ltexp2a  10528  leexp2a  10529  sqdivap  10540  qsqeqor  10586  expnbnd  10599  expsubapd  10620  lt2sqd  10640  le2sqd  10641  sq11d  10642  apexp1  10652  bcp1nk  10696  hashunlem  10739  zfz1isolem1  10775  cjap  10870  cnreim  10942  resqrexlem1arp  10969  resqrexlemp1rp  10970  resqrexlemglsq  10986  abs00ap  11026  absext  11027  absexpzap  11044  absrele  11047  sqrtmuld  11133  sqrtsq2d  11134  sqrtled  11135  sqrtltd  11136  sqr11d  11137  abs3lemd  11165  minmax  11193  xrmaxiflemlub  11211  xrltmaxsup  11220  xrminmax  11228  xrbdtri  11239  climuni  11256  2clim  11264  addcn2  11273  mulcn2  11275  fsum3  11350  mptfzshft  11405  fsumrev  11406  fisum0diag2  11410  modfsummodlemstep  11420  binomlem  11446  mertenslemi1  11498  fprodrev  11582  efcllemp  11621  p1modz1  11756  dvds1  11813  dvdsext  11815  mulmoddvds  11823  oexpneg  11836  evennn02n  11841  evennn2n  11842  bezoutlemmo  11961  mulgcd  11971  dvdssqlem  11985  rpmulgcd2  12049  isprm6  12101  sqrt2irraplemnn  12133  sqrt2irrap  12134  crth  12178  eulerthlemh  12185  prmdiveq  12190  powm2modprm  12206  modprm0  12208  pythagtriplem2  12220  pythagtriplem11  12228  pythagtriplem13  12230  pythagtrip  12237  pcid  12277  pcgcd1  12281  pcprmpw2  12286  dvdsprmpweqle  12290  pcaddlem  12292  pcadd  12293  fldivp1  12300  unennn  12352  ennnfonelemg  12358  ennnfonelemhf1o  12368  inffinp1  12384  isstructr  12431  ntrin  12918  topssnei  12956  restbasg  12962  cnntri  13018  txcn  13069  txlm  13073  cnmpt2res  13091  psmetlecl  13128  xmetlecl  13161  bldisj  13195  bdmet  13296  bdbl  13297  bdmopn  13298  xmetxp  13301  metcnp  13306  tgioo  13340  cncfmet  13373  dedekindeulemlub  13392  suplociccreex  13396  ellimc3apf  13423  limcimolemlt  13427  limccnp2cntop  13440  dvfvalap  13444  dvmulxxbr  13460  dvaddxx  13461  dvmulxx  13462  dviaddf  13463  dvimulf  13464  dvcoapbr  13465  dvmptclx  13474  cxplt3  13634  cxpltd  13642  cxpled  13643  cxplt3d  13648  cxple3d  13649  logbrec  13672  logbgcd1irraplemap  13681  lgslem1  13695  lgslem3  13697  lgsdirprm  13729  2sqlem7  13751