Theorem syl12anc 1236

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  1239  cocan1  5787  fliftfun  5796  isopolem  5822  f1oiso2  5827  caovcld  6027  caovcomd  6030  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  fidceq  6868  findcard2d  6890  diffifi  6893  tridc  6898  en2eqpr  6906  sbthlemi9  6963  supisolem  7006  ordiso2  7033  difinfsnlem  7097  difinfsn  7098  prarloclemup  7493  prarloc  7501  nqprl  7549  nqpru  7550  ltaddpr  7595  aptiprlemu  7638  archpr  7641  cauappcvgprlem2  7658  caucvgprlem2  7678  caucvgprprlem2  7708  suplocexprlemlub  7722  suplocexpr  7723  recexgt0sr  7771  archsr  7780  axpre-suploclemres  7899  conjmulap  8685  lerec2  8845  ledivp1  8859  cju  8917  nn2ge  8951  gtndiv  9347  supinfneg  9594  infsupneg  9595  z2ge  9825  iccssioo2  9945  fzrev3  10086  elfz1b  10089  exbtwnzlemstep  10247  exbtwnzlemex  10249  rebtwn2zlemstep  10252  rebtwn2z  10254  qbtwnre  10256  flqdiv  10320  frec2uzled  10428  seq3caopr  10482  iseqf1olemab  10488  iseqf1olemnanb  10489  expnegzap  10553  nn0ltexp2  10688  hashen  10763  hashunlem  10783  hashprg  10787  leisorel  10816  zfz1isolemiso  10818  seq3coll  10821  caucvgrelemrec  10987  resqrexlemex  11033  minmax  11237  xrminmax  11272  fsum2dlemstep  11441  fisumcom2  11445  zproddc  11586  fprod2dlemstep  11629  fprodcom2fi  11633  zsupcllemstep  11945  zsupssdc  11954  bezoutlemmain  11998  sqgcd  12029  pcpremul  12292  pceulem  12293  pceu  12294  pczpre  12296  pcdiv  12301  pcqmul  12302  pcqdiv  12306  pcexp  12308  pcdvdsb  12318  pcneg  12323  pcdvdstr  12325  pcgcd1  12326  pc2dvds  12328  pcz  12330  pcaddlem  12337  pcadd  12338  qexpz  12349  expnprm  12350  infpnlem2  12357  f1ocpbllem  12730  f1ovscpbl  12732  mndpropd  12840  grpsubpropd2  12974  ablnnncan  13124  ringpropd  13215  neiint  13581  restbasg  13604  iscnp4  13654  cnconst2  13669  cnpdis  13678  neitx  13704  upxp  13708  hmeoimaf1o  13750  blssexps  13865  blssex  13866  ssblex  13867  bdmopn  13940  xmettx  13946  metcnp3  13947  tgioo  13982  tgqioo  13983  sin0pilem2  14139  logbgcd1irr  14321  lgsval  14341  lgsfcl2  14343  lgsdir  14372  lgsdilem2  14373  lgsdi  14374  lgsne0  14375  pwle2  14684