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  13615  restbasg  13638  iscnp4  13688  cnconst2  13703  cnpdis  13712  neitx  13738  upxp  13742  hmeoimaf1o  13784  blssexps  13899  blssex  13900  ssblex  13901  bdmopn  13974  xmettx  13980  metcnp3  13981  tgioo  14016  tgqioo  14017  sin0pilem2  14173  logbgcd1irr  14355  lgsval  14375  lgsfcl2  14377  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  pwle2  14718