Theorem syl12anc 1214

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  1217  cocan1  5688  fliftfun  5697  isopolem  5723  f1oiso2  5728  caovcld  5924  caovcomd  5927  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  fidceq  6763  findcard2d  6785  diffifi  6788  tridc  6793  en2eqpr  6801  sbthlemi9  6853  supisolem  6895  ordiso2  6920  difinfsnlem  6984  difinfsn  6985  prarloclemup  7303  prarloc  7311  nqprl  7359  nqpru  7360  ltaddpr  7405  aptiprlemu  7448  archpr  7451  cauappcvgprlem2  7468  caucvgprlem2  7488  caucvgprprlem2  7518  suplocexprlemlub  7532  suplocexpr  7533  recexgt0sr  7581  archsr  7590  axpre-suploclemres  7709  conjmulap  8489  lerec2  8647  ledivp1  8661  cju  8719  nn2ge  8753  gtndiv  9146  supinfneg  9390  infsupneg  9391  z2ge  9609  iccssioo2  9729  fzrev3  9867  elfz1b  9870  exbtwnzlemstep  10025  exbtwnzlemex  10027  rebtwn2zlemstep  10030  rebtwn2z  10032  qbtwnre  10034  flqdiv  10094  frec2uzled  10202  seq3caopr  10256  iseqf1olemab  10262  iseqf1olemnanb  10263  expnegzap  10327  hashen  10530  hashunlem  10550  hashprg  10554  leisorel  10580  zfz1isolemiso  10582  seq3coll  10585  caucvgrelemrec  10751  resqrexlemex  10797  minmax  11001  xrminmax  11034  fsum2dlemstep  11203  fisumcom2  11207  zsupcllemstep  11638  bezoutlemmain  11686  sqgcd  11717  neiint  12314  restbasg  12337  iscnp4  12387  cnconst2  12402  cnpdis  12411  neitx  12437  upxp  12441  hmeoimaf1o  12483  blssexps  12598  blssex  12599  ssblex  12600  bdmopn  12673  xmettx  12679  metcnp3  12680  tgioo  12715  tgqioo  12716  sin0pilem2  12863  pwle2  13193