Theorem syl12anc 1269

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  1272  cocan1  5917  fliftfun  5926  isopolem  5952  f1oiso2  5957  caovcld  6165  caovcomd  6168  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  fidceq  7039  findcard2d  7061  diffifi  7064  tridc  7069  en2eqpr  7077  sbthlemi9  7140  supisolem  7183  ordiso2  7210  difinfsnlem  7274  difinfsn  7275  pr2cv1  7376  prarloclemup  7690  prarloc  7698  nqprl  7746  nqpru  7747  ltaddpr  7792  aptiprlemu  7835  archpr  7838  cauappcvgprlem2  7855  caucvgprlem2  7875  caucvgprprlem2  7905  suplocexprlemlub  7919  suplocexpr  7920  recexgt0sr  7968  archsr  7977  axpre-suploclemres  8096  conjmulap  8884  lerec2  9044  ledivp1  9058  cju  9116  nn2ge  9151  gtndiv  9550  supinfneg  9798  infsupneg  9799  z2ge  10030  iccssioo2  10150  fzrev3  10291  elfz1b  10294  zsupcllemstep  10457  zsupssdc  10466  exbtwnzlemstep  10475  exbtwnzlemex  10477  rebtwn2zlemstep  10480  rebtwn2z  10482  qbtwnre  10484  flqdiv  10551  frec2uzled  10659  seq3caopr  10725  seqcaoprg  10726  iseqf1olemab  10732  iseqf1olemnanb  10733  seqf1oglem1  10749  expnegzap  10803  nn0ltexp2  10939  hashen  11014  hashunlem  11034  hashprg  11038  leisorel  11067  zfz1isolemiso  11069  seq3coll  11072  swrdccat3b  11280  caucvgrelemrec  11498  resqrexlemex  11544  minmax  11749  xrminmax  11784  fsum2dlemstep  11953  fisumcom2  11957  zproddc  12098  fprod2dlemstep  12141  fprodcom2fi  12145  bezoutlemmain  12527  sqgcd  12558  pcpremul  12824  pceulem  12825  pceu  12826  pczpre  12828  pcdiv  12833  pcqmul  12834  pcqdiv  12838  pcexp  12840  pcdvdsb  12851  pcneg  12856  pcdvdstr  12858  pcgcd1  12859  pc2dvds  12861  pcz  12863  pcaddlem  12870  pcadd  12871  qexpz  12883  expnprm  12884  infpnlem2  12891  f1ocpbllem  13351  f1ovscpbl  13353  sgrppropd  13454  mndpropd  13481  grpsubpropd2  13646  f1ghm0to0  13817  ablnnncan  13868  rngpropd  13926  ringpropd  14009  lmodprop2d  14320  lsspropdg  14403  neiint  14827  restbasg  14850  iscnp4  14900  cnconst2  14915  cnpdis  14924  neitx  14950  upxp  14954  hmeoimaf1o  14996  blssexps  15111  blssex  15112  ssblex  15113  bdmopn  15186  xmettx  15192  metcnp3  15193  tgioo  15236  tgqioo  15237  dvmptfsum  15407  elply2  15417  sin0pilem2  15464  logbgcd1irr  15649  perfect  15683  lgsval  15691  lgsfcl2  15693  lgsdir  15722  lgsdilem2  15723  lgsdi  15724  lgsne0  15725  1dom1el  16378  pwle2  16393