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  5484  tfrexlem  6310  th3qlem1  6611  enpr2d  6791  ssenen  6825  phplem4dom  6836  phplem4on  6841  fiunsnnn  6855  findcard2sd  6866  unsnfi  6892  sbthlemi9  6938  endjusym  7069  endjudisj  7174  djuen  7175  ltanqg  7349  ltmnqg  7350  ltnnnq  7372  addcmpblnq0  7392  addlocprlemeqgt  7481  distrlem1prl  7531  distrlem1pru  7532  distrlem4prl  7533  distrlem4pru  7534  addcanprleml  7563  recexprlem1ssl  7582  caucvgprlemloc  7624  caucvgprprlemloccalc  7633  mulcmpblnr  7690  ltasrg  7719  recexgt0sr  7722  mulextsr1lem  7729  mulextsr1  7730  srpospr  7732  prsrlt  7736  ltpsrprg  7752  mappsrprg  7753  pitonnlem1p1  7795  recidpirq  7807  axpre-ltadd  7835  mulgt0d  8029  mul4d  8061  add4d  8075  add42d  8076  subcan  8161  addsub4d  8264  subadd4d  8265  sub4d  8266  2addsubd  8267  addsubeq4d  8268  muladdd  8322  mulsubd  8323  addgegt0d  8425  addgtge0d  8426  addge0d  8428  le2addd  8469  le2subd  8470  ltleaddd  8471  leltaddd  8472  lt2subd  8474  apreap  8493  apsym  8512  apcotr  8513  apadd1  8514  apneg  8517  mulext1  8518  mulap0r  8521  mulge0d  8527  mulap0d  8563  divdivdivap  8617  divcanap5  8618  divap0d  8710  recdivapd  8711  recdivap2d  8712  divcanap6d  8713  ddcanapd  8714  rec11apd  8715  divmuldivapd  8736  divmuleqapd  8737  subrecapd  8745  prodgt0  8755  lt2msq  8789  ledivdiv  8793  lediv12a  8797  recreclt  8803  divgt0d  8838  mulgt1d  8839  lemulge11d  8840  lemulge12d  8841  ltmul12ad  8844  lemul12ad  8845  lemul12bd  8846  nndivtr  8907  qreccl  9588  ledivdivd  9666  lediv12ad  9700  lt2mul2divd  9709  xlt2add  9824  xleaddadd  9831  iccss2  9888  iccssico2  9891  lincmb01cmp  9947  iccf1o  9948  fzrev2i  10029  qtri3or  10186  elicore  10210  2tnp1ge0ge0  10244  modqid  10292  q0mod  10298  q1mod  10299  modqabs  10300  modqadd1  10304  mulqaddmodid  10307  mulp1mod1  10308  modqmuladd  10309  modqmuladdnn0  10311  qnegmod  10312  m1modnnsub1  10313  addmodid  10315  modqm1p1mod0  10318  modqltm1p1mod  10319  modqmul1  10320  q2submod  10328  modifeq2int  10329  modaddmodup  10330  modaddmodlo  10331  modqaddmulmod  10334  modqsubdir  10336  modqeqmodmin  10337  modsumfzodifsn  10339  addmodlteq  10341  frecfzennn  10369  ser3mono  10421  expcl2lemap  10475  mulexpzap  10503  expaddzaplem  10506  expaddzap  10507  expmulzap  10509  ltexp2a  10515  leexp2a  10516  sqdivap  10527  qsqeqor  10573  expnbnd  10586  expsubapd  10607  lt2sqd  10627  le2sqd  10628  sq11d  10629  apexp1  10639  bcp1nk  10683  hashunlem  10726  zfz1isolem1  10762  cjap  10857  cnreim  10929  resqrexlem1arp  10956  resqrexlemp1rp  10957  resqrexlemglsq  10973  abs00ap  11013  absext  11014  absexpzap  11031  absrele  11034  sqrtmuld  11120  sqrtsq2d  11121  sqrtled  11122  sqrtltd  11123  sqr11d  11124  abs3lemd  11152  minmax  11180  xrmaxiflemlub  11198  xrltmaxsup  11207  xrminmax  11215  xrbdtri  11226  climuni  11243  2clim  11251  addcn2  11260  mulcn2  11262  fsum3  11337  mptfzshft  11392  fsumrev  11393  fisum0diag2  11397  modfsummodlemstep  11407  binomlem  11433  mertenslemi1  11485  fprodrev  11569  efcllemp  11608  p1modz1  11743  dvds1  11800  dvdsext  11802  mulmoddvds  11810  oexpneg  11823  evennn02n  11828  evennn2n  11829  bezoutlemmo  11948  mulgcd  11958  dvdssqlem  11972  rpmulgcd2  12036  isprm6  12088  sqrt2irraplemnn  12120  sqrt2irrap  12121  crth  12165  eulerthlemh  12172  prmdiveq  12177  powm2modprm  12193  modprm0  12195  pythagtriplem2  12207  pythagtriplem11  12215  pythagtriplem13  12217  pythagtrip  12224  pcid  12264  pcgcd1  12268  pcprmpw2  12273  dvdsprmpweqle  12277  pcaddlem  12279  pcadd  12280  fldivp1  12287  unennn  12339  ennnfonelemg  12345  ennnfonelemhf1o  12355  inffinp1  12371  isstructr  12418  ntrin  12877  topssnei  12915  restbasg  12921  cnntri  12977  txcn  13028  txlm  13032  cnmpt2res  13050  psmetlecl  13087  xmetlecl  13120  bldisj  13154  bdmet  13255  bdbl  13256  bdmopn  13257  xmetxp  13260  metcnp  13265  tgioo  13299  cncfmet  13332  dedekindeulemlub  13351  suplociccreex  13355  ellimc3apf  13382  limcimolemlt  13386  limccnp2cntop  13399  dvfvalap  13403  dvmulxxbr  13419  dvaddxx  13420  dvmulxx  13421  dviaddf  13422  dvimulf  13423  dvcoapbr  13424  dvmptclx  13433  cxplt3  13593  cxpltd  13601  cxpled  13602  cxplt3d  13607  cxple3d  13608  logbrec  13631  logbgcd1irraplemap  13640  lgslem1  13654  lgslem3  13656  lgsdirprm  13688  2sqlem7  13710