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  5920  fliftfun  5929  isopolem  5955  f1oiso2  5960  caovcld  6168  caovcomd  6171  tfrlemisucaccv  6482  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  fidceq  7044  findcard2d  7066  diffifi  7069  tridc  7075  en2eqpr  7085  sbthlemi9  7148  supisolem  7191  ordiso2  7218  difinfsnlem  7282  difinfsn  7283  pr2cv1  7384  prarloclemup  7698  prarloc  7706  nqprl  7754  nqpru  7755  ltaddpr  7800  aptiprlemu  7843  archpr  7846  cauappcvgprlem2  7863  caucvgprlem2  7883  caucvgprprlem2  7913  suplocexprlemlub  7927  suplocexpr  7928  recexgt0sr  7976  archsr  7985  axpre-suploclemres  8104  conjmulap  8892  lerec2  9052  ledivp1  9066  cju  9124  nn2ge  9159  gtndiv  9558  supinfneg  9807  infsupneg  9808  z2ge  10039  iccssioo2  10159  fzrev3  10300  elfz1b  10303  zsupcllemstep  10466  zsupssdc  10475  exbtwnzlemstep  10484  exbtwnzlemex  10486  rebtwn2zlemstep  10489  rebtwn2z  10491  qbtwnre  10493  flqdiv  10560  frec2uzled  10668  seq3caopr  10734  seqcaoprg  10735  iseqf1olemab  10741  iseqf1olemnanb  10742  seqf1oglem1  10758  expnegzap  10812  nn0ltexp2  10948  hashen  11023  hashunlem  11043  hashprg  11048  leisorel  11077  zfz1isolemiso  11079  seq3coll  11082  swrdccat3b  11293  caucvgrelemrec  11511  resqrexlemex  11557  minmax  11762  xrminmax  11797  fsum2dlemstep  11966  fisumcom2  11970  zproddc  12111  fprod2dlemstep  12154  fprodcom2fi  12158  bezoutlemmain  12540  sqgcd  12571  pcpremul  12837  pceulem  12838  pceu  12839  pczpre  12841  pcdiv  12846  pcqmul  12847  pcqdiv  12851  pcexp  12853  pcdvdsb  12864  pcneg  12869  pcdvdstr  12871  pcgcd1  12872  pc2dvds  12874  pcz  12876  pcaddlem  12883  pcadd  12884  qexpz  12896  expnprm  12897  infpnlem2  12904  f1ocpbllem  13364  f1ovscpbl  13366  sgrppropd  13467  mndpropd  13494  grpsubpropd2  13659  f1ghm0to0  13830  ablnnncan  13881  rngpropd  13939  ringpropd  14022  lmodprop2d  14333  lsspropdg  14416  neiint  14840  restbasg  14863  iscnp4  14913  cnconst2  14928  cnpdis  14937  neitx  14963  upxp  14967  hmeoimaf1o  15009  blssexps  15124  blssex  15125  ssblex  15126  bdmopn  15199  xmettx  15205  metcnp3  15206  tgioo  15249  tgqioo  15250  dvmptfsum  15420  elply2  15430  sin0pilem2  15477  logbgcd1irr  15662  perfect  15696  lgsval  15704  lgsfcl2  15706  lgsdir  15735  lgsdilem2  15736  lgsdi  15737  lgsne0  15738  1dom1el  16463  pwle2  16477