Theorem syl12anc 1271

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
syl12anc.4	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
syl12anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl12anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca32 310	. 2 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	4, 5	syl 14	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:  syl22anc  1274  cocan1  5928  fliftfun  5937  isopolem  5963  f1oiso2  5968  caovcld  6176  caovcomd  6179  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  1dom1el  6993  fidceq  7056  findcard2d  7080  diffifi  7083  tridc  7089  en2eqpr  7099  sbthlemi9  7164  supisolem  7207  ordiso2  7234  difinfsnlem  7298  difinfsn  7299  pr2cv1  7400  prarloclemup  7715  prarloc  7723  nqprl  7771  nqpru  7772  ltaddpr  7817  aptiprlemu  7860  archpr  7863  cauappcvgprlem2  7880  caucvgprlem2  7900  caucvgprprlem2  7930  suplocexprlemlub  7944  suplocexpr  7945  recexgt0sr  7993  archsr  8002  axpre-suploclemres  8121  conjmulap  8909  lerec2  9069  ledivp1  9083  cju  9141  nn2ge  9176  gtndiv  9575  supinfneg  9829  infsupneg  9830  z2ge  10061  iccssioo2  10181  fzrev3  10322  elfz1b  10325  zsupcllemstep  10490  zsupssdc  10499  exbtwnzlemstep  10508  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnre  10517  flqdiv  10584  frec2uzled  10692  seq3caopr  10758  seqcaoprg  10759  iseqf1olemab  10765  iseqf1olemnanb  10766  seqf1oglem1  10782  expnegzap  10836  nn0ltexp2  10972  hashen  11047  hashunlem  11068  hashprg  11073  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  swrdccat3b  11322  caucvgrelemrec  11541  resqrexlemex  11587  minmax  11792  xrminmax  11827  fsum2dlemstep  11997  fisumcom2  12001  zproddc  12142  fprod2dlemstep  12185  fprodcom2fi  12189  bezoutlemmain  12571  sqgcd  12602  pcpremul  12868  pceulem  12869  pceu  12870  pczpre  12872  pcdiv  12877  pcqmul  12878  pcqdiv  12882  pcexp  12884  pcdvdsb  12895  pcneg  12900  pcdvdstr  12902  pcgcd1  12903  pc2dvds  12905  pcz  12907  pcaddlem  12914  pcadd  12915  qexpz  12927  expnprm  12928  infpnlem2  12935  f1ocpbllem  13395  f1ovscpbl  13397  sgrppropd  13498  mndpropd  13525  grpsubpropd2  13690  f1ghm0to0  13861  ablnnncan  13912  rngpropd  13971  ringpropd  14054  lmodprop2d  14365  lsspropdg  14448  neiint  14872  restbasg  14895  iscnp4  14945  cnconst2  14960  cnpdis  14969  neitx  14995  upxp  14999  hmeoimaf1o  15041  blssexps  15156  blssex  15157  ssblex  15158  bdmopn  15231  xmettx  15237  metcnp3  15238  tgioo  15281  tgqioo  15282  dvmptfsum  15452  elply2  15462  sin0pilem2  15509  logbgcd1irr  15694  perfect  15728  lgsval  15736  lgsfcl2  15738  lgsdir  15767  lgsdilem2  15768  lgsdi  15769  lgsne0  15770  clwwlknonex2e  16294  pwle2  16620