Theorem syl22anc 1279

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 1276	1 ⊢ (𝜑 → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  f1oprg  5685  tfrexlem  6605  th3qlem1  6911  en2prd  7106  enpr2d  7111  ssenen  7152  phplem4dom  7163  phplem4on  7169  fiunsnnn  7185  findcard2sd  7196  unsnfi  7226  sbthlemi9  7282  fsuppcorn  7301  endjusym  7436  endjudisj  7566  djuen  7567  ltanqg  7767  ltmnqg  7768  ltnnnq  7790  addcmpblnq0  7810  addlocprlemeqgt  7899  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  addcanprleml  7981  recexprlem1ssl  8000  caucvgprlemloc  8042  caucvgprprlemloccalc  8051  mulcmpblnr  8108  ltasrg  8137  recexgt0sr  8140  mulextsr1lem  8147  mulextsr1  8148  srpospr  8150  prsrlt  8154  ltpsrprg  8170  mappsrprg  8171  pitonnlem1p1  8213  recidpirq  8225  axpre-ltadd  8253  mulgt0d  8449  mul4d  8481  add4d  8495  add42d  8496  subcan  8581  addsub4d  8684  subadd4d  8685  sub4d  8686  2addsubd  8687  addsubeq4d  8688  muladdd  8743  mulsubd  8744  addgegt0d  8847  addgtge0d  8848  addge0d  8850  le2addd  8892  le2subd  8893  ltleaddd  8894  leltaddd  8895  lt2subd  8897  apreap  8916  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  mulap0r  8944  mulge0d  8950  mulap0d  8987  divdivdivap  9044  divcanap5  9045  divap0d  9137  recdivapd  9138  recdivap2d  9139  divcanap6d  9140  ddcanapd  9141  rec11apd  9142  divmuldivapd  9163  divmuleqapd  9164  subrecapd  9172  prodgt0  9183  lt2msq  9217  ledivdiv  9221  lediv12a  9225  recreclt  9231  divgt0d  9266  mulgt1d  9267  lemulge11d  9268  lemulge12d  9269  ltmul12ad  9272  lemul12ad  9273  lemul12bd  9274  nndivtr  9347  qreccl  10044  ledivdivd  10125  lediv12ad  10159  lt2mul2divd  10168  xlt2add  10284  xleaddadd  10291  iccss2  10348  iccssico2  10351  lincmb01cmp  10407  iccf1o  10409  fzrev2i  10495  qtri3or  10677  elicore  10703  2tnp1ge0ge0  10738  modqid  10788  q0mod  10794  q1mod  10795  modqabs  10796  modqadd1  10800  mulqaddmodid  10803  mulp1mod1  10804  modqmuladd  10805  modqmuladdnn0  10807  qnegmod  10808  m1modnnsub1  10809  addmodid  10811  modqm1p1mod0  10814  modqltm1p1mod  10815  modqmul1  10816  q2submod  10824  modifeq2int  10825  modaddmodup  10826  modaddmodlo  10827  modqaddmulmod  10830  modqsubdir  10832  modqeqmodmin  10833  modsumfzodifsn  10835  addmodlteq  10837  frecfzennn  10865  ser3mono  10926  expcl2lemap  10990  mulexpzap  11018  expaddzaplem  11021  expaddzap  11022  expmulzap  11024  ltexp2a  11030  leexp2a  11031  sqdivap  11042  qsqeqor  11089  expnbnd  11103  expsubapd  11124  lt2sqd  11144  le2sqd  11145  sq11d  11146  apexp1  11158  bcp1nk  11202  hashunlem  11246  hashf1lem1  11287  zfz1isolem1  11294  hashtpgim  11299  sq01  11662  cjap  11674  cnreim  11746  resqrexlem1arp  11773  resqrexlemp1rp  11774  resqrexlemglsq  11790  abs00ap  11830  absext  11831  absexpzap  11848  absrele  11851  sqrtmuld  11937  sqrtsq2d  11938  sqrtled  11939  sqrtltd  11940  sqr11d  11941  abs3lemd  11969  minmax  11998  xrmaxiflemlub  12016  xrltmaxsup  12025  xrminmax  12033  xrbdtri  12044  climuni  12061  2clim  12069  addcn2  12078  mulcn2  12080  fsum3  12156  mptfzshft  12211  fsumrev  12212  fisum0diag2  12216  modfsummodlemstep  12226  binomlem  12252  mertenslemi1  12304  fprodrev  12388  efcllemp  12427  p1modz1  12563  dvds1  12622  dvdsext  12624  mulmoddvds  12632  oexpneg  12646  evennn02n  12651  evennn2n  12652  bitsinv1  12731  bezoutlemmo  12785  mulgcd  12795  dvdssqlem  12809  rpmulgcd2  12875  isprm6  12927  sqrt2irraplemnn  12959  sqrt2irrap  12960  crth  13004  eulerthlemh  13011  prmdiveq  13016  powm2modprm  13033  modprm0  13035  pythagtriplem2  13047  pythagtriplem11  13055  pythagtriplem13  13057  pythagtrip  13064  pcid  13105  pcgcd1  13109  pcprmpw2  13114  dvdsprmpweqle  13118  pcaddlem  13120  pcadd  13121  fldivp1  13129  4sqlem12  13183  4sqlem14  13185  4sqlem15  13186  4sqlem16  13187  ballotfilemsima  13261  ballotfilemfrceq  13274  unennn  13290  ennnfonelemg  13296  ennnfonelemhf1o  13306  inffinp1  13322  isstructr  13369  setscomd  13395  imasbas  13630  imasplusg  13631  imasmulr  13632  subm0  13791  gzsumshift  14151  gsump1  14159  lssvancl1  14706  lssvnegcl  14715  lspprvacl  14752  lspsneli  14754  lspsn  14755  znf1o  14988  ntrin  15227  topssnei  15265  restbasg  15271  cnntri  15327  txcn  15378  txlm  15382  cnmpt2res  15400  psmetlecl  15437  xmetlecl  15470  bldisj  15504  bdmet  15605  bdbl  15606  bdmopn  15607  xmetxp  15610  metcnp  15615  tgioo  15657  cncfmet  15695  dedekindeulemlub  15723  suplociccreex  15727  ellimc3apf  15763  limcimolemlt  15767  limccnp2cntop  15780  dvfvalap  15784  dvidsslem  15796  dvmulxxbr  15805  dvaddxx  15806  dvmulxx  15807  dviaddf  15808  dvimulf  15809  dvcoapbr  15810  dvmptclx  15821  cxplt3  16028  cxpltd  16036  cxpled  16037  cxplt3d  16043  cxple3d  16044  logbrec  16068  logbgcd1irraplemap  16077  log2tlbndlog2  16088  birthdaylem3  16095  pellexlem1  16097  pellexlem2  16098  wilthlem1  16100  mpodvdsmulf1o  16110  bclbnd  16127  lgslem1  16131  lgslem3  16133  lgsdirprm  16165  gausslemma2dlem1f1o  16191  gausslemma2dlem6  16198  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem4  16204  lgseisen  16205  lgsquadlem1  16208  lgsquad2lem1  16212  lgsquad3  16215  m1lgs  16216  2lgslem1a1  16217  2sqlem7  16252  usgredg2v  16477  vtxd0nedgbfi  16552  clwwlknonex2  16692