Theorem syl31anc 1255

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

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

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 985

This theorem is referenced by:  syl32anc  1260  stoic4b  1455  enq0tr  7589  ltmul12a  8975  lt2msq1  9000  ledivp1  9018  lemul1ad  9054  lemul2ad  9055  lediv2ad  9883  xaddge0  10042  difelfznle  10299  expubnd  10785  nn0leexp2  10899  expcanlem  10904  expcand  10906  swrds1  11166  ccatswrd  11168  pfxfv  11182  swrdccatin1  11223  pfxccatin12lem3  11230  xrmaxaddlem  11737  mertenslemi1  12012  eftlub  12167  dvdsadd  12313  3dvds  12341  divalgmod  12404  bitsfzolem  12431  bitsfzo  12432  bitsmod  12433  bitsinv1lem  12438  gcdzeq  12509  rplpwr  12514  sqgcd  12516  bezoutr  12519  rpmulgcd2  12583  rpdvds  12587  isprm5  12630  divgcdodd  12631  oddpwdclemxy  12657  divnumden  12684  crth  12712  phimullem  12713  coprimeprodsq2  12747  pythagtriplem19  12771  pclemub  12776  pcpre1  12781  pcidlem  12812  pockthlem  12845  prmunb  12851  kerf1ghm  13777  elrhmunit  14106  rrgnz  14197  znunit  14588  xblss2ps  15043  xblss2  15044  metcnpi3  15156  limcimolemlt  15303  limccnp2cntop  15316  dvmulxxbr  15341  dvcoapbr  15346  ltexp2d  15581  mpodvdsmulf1o  15629  lgsquad2lem2  15726  2lgsoddprmlem1  15749  2sqlem8a  15766  2sqlem8  15767