Theorem syl31anc 1274

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 1201	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		sylXanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 411	1 ⊢ (𝜑 → 𝜂)

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

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 1004

This theorem is referenced by:  syl32anc  1279  stoic4b  1475  enq0tr  7647  ltmul12a  9033  lt2msq1  9058  ledivp1  9076  lemul1ad  9112  lemul2ad  9113  lediv2ad  9947  xaddge0  10106  difelfznle  10363  expubnd  10851  nn0leexp2  10965  expcanlem  10970  expcand  10972  swrds1  11242  ccatswrd  11244  pfxfv  11258  swrdccatin1  11299  pfxccatin12lem3  11306  xrmaxaddlem  11814  mertenslemi1  12089  eftlub  12244  dvdsadd  12390  3dvds  12418  divalgmod  12481  bitsfzolem  12508  bitsfzo  12509  bitsmod  12510  bitsinv1lem  12515  gcdzeq  12586  rplpwr  12591  sqgcd  12593  bezoutr  12596  rpmulgcd2  12660  rpdvds  12664  isprm5  12707  divgcdodd  12708  oddpwdclemxy  12734  divnumden  12761  crth  12789  phimullem  12790  coprimeprodsq2  12824  pythagtriplem19  12848  pclemub  12853  pcpre1  12858  pcidlem  12889  pockthlem  12922  prmunb  12928  kerf1ghm  13854  elrhmunit  14184  rrgnz  14275  znunit  14666  xblss2ps  15121  xblss2  15122  metcnpi3  15234  limcimolemlt  15381  limccnp2cntop  15394  dvmulxxbr  15419  dvcoapbr  15424  ltexp2d  15659  mpodvdsmulf1o  15707  lgsquad2lem2  15804  2lgsoddprmlem1  15827  2sqlem8a  15844  2sqlem8  15845