Theorem syl31anc 1253

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl31anc.5	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl31anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl31anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1180	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		sylXanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 411	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  syl32anc  1258  stoic4b  1453  enq0tr  7554  ltmul12a  8940  lt2msq1  8965  ledivp1  8983  lemul1ad  9019  lemul2ad  9020  lediv2ad  9848  xaddge0  10007  difelfznle  10264  expubnd  10748  nn0leexp2  10862  expcanlem  10867  expcand  10869  swrds1  11129  ccatswrd  11131  pfxfv  11143  xrmaxaddlem  11615  mertenslemi1  11890  eftlub  12045  dvdsadd  12191  3dvds  12219  divalgmod  12282  bitsfzolem  12309  bitsfzo  12310  bitsmod  12311  bitsinv1lem  12316  gcdzeq  12387  rplpwr  12392  sqgcd  12394  bezoutr  12397  rpmulgcd2  12461  rpdvds  12465  isprm5  12508  divgcdodd  12509  oddpwdclemxy  12535  divnumden  12562  crth  12590  phimullem  12591  coprimeprodsq2  12625  pythagtriplem19  12649  pclemub  12654  pcpre1  12659  pcidlem  12690  pockthlem  12723  prmunb  12729  kerf1ghm  13654  elrhmunit  13983  rrgnz  14074  znunit  14465  xblss2ps  14920  xblss2  14921  metcnpi3  15033  limcimolemlt  15180  limccnp2cntop  15193  dvmulxxbr  15218  dvcoapbr  15223  ltexp2d  15458  mpodvdsmulf1o  15506  lgsquad2lem2  15603  2lgsoddprmlem1  15626  2sqlem8a  15643  2sqlem8  15644