Theorem syl22anc 1170

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  f1oprg  5188  tfrexlem  5971  th3qlem1  6231  phplem4dom  6348  phplem4on  6353  fiunsnnn  6365  findcard2sd  6376  unsnfi  6384  ltanqg  6590  ltmnqg  6591  ltnnnq  6613  addcmpblnq0  6633  addlocprlemeqgt  6722  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  addcanprleml  6804  recexprlem1ssl  6823  caucvgprlemloc  6865  caucvgprprlemloccalc  6874  mulcmpblnr  6918  ltasrg  6947  recexgt0sr  6950  mulextsr1lem  6956  mulextsr1  6957  srpospr  6959  prsrlt  6963  pitonnlem1p1  7014  recidpirq  7026  axpre-ltadd  7052  mulgt0d  7232  mul4d  7263  add4d  7277  add42d  7278  subcan  7363  addsub4d  7466  subadd4d  7467  sub4d  7468  2addsubd  7469  addsubeq4d  7470  muladdd  7520  mulsubd  7521  addgegt0d  7620  addge0d  7622  le2addd  7663  le2subd  7664  ltleaddd  7665  leltaddd  7666  lt2subd  7668  apreap  7687  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  mulap0r  7715  mulge0d  7721  mulap0d  7748  divdivdivap  7801  divcanap5  7802  divap0d  7893  recdivapd  7894  recdivap2d  7895  divcanap6d  7896  ddcanapd  7897  rec11apd  7898  divmuldivapd  7918  prodgt0  7930  lt2msq  7964  ledivdiv  7968  lediv12a  7972  recreclt  7978  divgt0d  8013  mulgt1d  8014  lemulge11d  8015  lemulge12d  8016  ltmul12ad  8019  lemul12ad  8020  lemul12bd  8021  nndivtr  8080  qreccl  8727  ledivdivd  8799  lediv12ad  8833  lt2mul2divd  8836  iccss2  8967  iccssico2  8970  lincmb01cmp  9025  iccf1o  9026  fzrev2i  9103  qtri3or  9252  2tnp1ge0ge0  9303  modqid  9351  q0mod  9357  q1mod  9358  modqabs  9359  modqadd1  9363  mulqaddmodid  9366  mulp1mod1  9367  modqmuladd  9368  modqmuladdnn0  9370  qnegmod  9371  m1modnnsub1  9372  addmodid  9374  modqm1p1mod0  9377  modqltm1p1mod  9378  modqmul1  9379  q2submod  9387  modifeq2int  9388  modaddmodup  9389  modaddmodlo  9390  modqaddmulmod  9393  modqsubdir  9395  modqeqmodmin  9396  modsumfzodifsn  9398  addmodlteq  9400  frecfzennn  9419  isermono  9457  expcl2lemap  9488  mulexpzap  9516  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  ltexp2a  9528  leexp2a  9529  sqdivap  9540  expnbnd  9596  expsubapd  9616  lt2sqd  9636  le2sqd  9637  sq11d  9638  bcp1nk  9689  cjap  9793  resqrexlem1arp  9891  resqrexlemp1rp  9892  resqrexlemglsq  9908  abs00ap  9948  absext  9949  absexpzap  9966  absrele  9969  sqrtmuld  10055  sqrtsq2d  10056  sqrtled  10057  sqrtltd  10058  sqr11d  10059  abs3lemd  10087  minmax  10112  climuni  10132  2clim  10140  addcn2  10149  mulcn2  10151  dvds1  10253  dvdsext  10255  mulmoddvds  10263  oexpneg  10276  evennn02n  10282  evennn2n  10283  bezoutlemmo  10395  mulgcd  10405  dvdssqlem  10419  rpmulgcd2  10477  isprm6  10526  sqrt2irraplemnn  10557  sqrt2irrap  10558