Theorem syl12anc 1226

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 308	. 2 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  syl22anc  1229  cocan1  5754  fliftfun  5763  isopolem  5789  f1oiso2  5794  caovcld  5991  caovcomd  5994  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  fidceq  6831  findcard2d  6853  diffifi  6856  tridc  6861  en2eqpr  6869  sbthlemi9  6926  supisolem  6969  ordiso2  6996  difinfsnlem  7060  difinfsn  7061  prarloclemup  7432  prarloc  7440  nqprl  7488  nqpru  7489  ltaddpr  7534  aptiprlemu  7577  archpr  7580  cauappcvgprlem2  7597  caucvgprlem2  7617  caucvgprprlem2  7647  suplocexprlemlub  7661  suplocexpr  7662  recexgt0sr  7710  archsr  7719  axpre-suploclemres  7838  conjmulap  8621  lerec2  8780  ledivp1  8794  cju  8852  nn2ge  8886  gtndiv  9282  supinfneg  9529  infsupneg  9530  z2ge  9758  iccssioo2  9878  fzrev3  10018  elfz1b  10021  exbtwnzlemstep  10179  exbtwnzlemex  10181  rebtwn2zlemstep  10184  rebtwn2z  10186  qbtwnre  10188  flqdiv  10252  frec2uzled  10360  seq3caopr  10414  iseqf1olemab  10420  iseqf1olemnanb  10421  expnegzap  10485  nn0ltexp2  10619  hashen  10693  hashunlem  10713  hashprg  10717  leisorel  10746  zfz1isolemiso  10748  seq3coll  10751  caucvgrelemrec  10917  resqrexlemex  10963  minmax  11167  xrminmax  11202  fsum2dlemstep  11371  fisumcom2  11375  zproddc  11516  fprod2dlemstep  11559  fprodcom2fi  11563  zsupcllemstep  11874  zsupssdc  11883  bezoutlemmain  11927  sqgcd  11958  pcpremul  12221  pceulem  12222  pceu  12223  pczpre  12225  pcdiv  12230  pcqmul  12231  pcqdiv  12235  pcexp  12237  pcdvdsb  12247  pcneg  12252  pcdvdstr  12254  pcgcd1  12255  pc2dvds  12257  pcz  12259  pcaddlem  12266  pcadd  12267  qexpz  12278  expnprm  12279  infpnlem2  12286  neiint  12745  restbasg  12768  iscnp4  12818  cnconst2  12833  cnpdis  12842  neitx  12868  upxp  12872  hmeoimaf1o  12914  blssexps  13029  blssex  13030  ssblex  13031  bdmopn  13104  xmettx  13110  metcnp3  13111  tgioo  13146  tgqioo  13147  sin0pilem2  13303  logbgcd1irr  13485  lgsval  13505  lgsfcl2  13507  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  pwle2  13838