Theorem syl13anc 1280

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

Hypotheses

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

Assertion

Ref	Expression
syl13anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl13anc

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl23anc  1285  syl33anc  1293  caovassd  6252  caovcand  6255  caovordid  6259  caovordd  6261  caovdid  6268  caovdird  6271  swoer  6839  swoord1  6840  swoord2  6841  fimax2gtrilemstep  7210  iunfidisj  7265  ssfii  7314  suplub2ti  7348  prarloclem3  7871  fzosubel3  10632  seq3split  10947  seqsplitg  10948  seq3caopr  10954  seqcaoprg  10955  zsumdc  12177  fsumiun  12270  divalglemex  12715  pcgcd1  13137  strle1g  13520  mnd32g  13800  mnd12g  13801  mnd4g  13802  ismndd  13810  mndinvmod  13818  imasmnd  13820  grpassd  13877  grpasscan2  13929  grpidrcan  13930  grpidlcan  13931  grpinvinv  13932  grplmulf1o  13939  grpinvssd  13942  grpinvadd  13943  grpsubrcan  13946  grpsubadd  13953  grpaddsubass  13955  grppncan  13956  grpsubsub4  13958  grppnpcan2  13959  grpnpncan  13960  grpnpncan0  13961  grpnnncan2  13962  dfgrp3mlem  13963  dfgrp3m  13964  grplactcnv  13967  imasgrp  13974  mhmmnd  13979  mulgaddcomlem  14008  mulgaddcom  14009  mulgnn0dir  14015  mulgdirlem  14016  mulgneg2  14019  mulgnnass  14020  mulgnn0ass  14021  mulgass  14022  mulgmodid  14024  nsgconj  14069  isnsg3  14070  nmzsubg  14073  ssnmz  14074  eqger  14087  eqgcpbl  14091  conjghm  14139  conjnmz  14142  conjnmzb  14143  cntzsgrpcl  14168  cntzsubm  14171  cntzsubg  14172  abl32  14201  abladdsub4  14209  abladdsub  14210  ablpncan2  14211  ablsubsub  14213  gsummptfidmsplit  14255  prdssgrpd  14299  prdsmndd  14302  rngass  14346  rnglz  14352  rngrz  14353  rngmneg1  14354  rngmneg2  14355  rngsubdi  14358  rngsubdir  14359  imasrng  14363  srgass  14383  srgmulgass  14401  srgpcomp  14402  srgpcompp  14403  srgpcomppsc  14404  ringass  14428  ringadd2  14440  ringo2times  14441  ringcom  14444  ringlz  14456  ringrz  14457  ringnegl  14464  ringnegr  14465  ringmneg1  14466  ringmneg2  14467  ringsubdi  14469  ringsubdir  14470  mulgass2  14471  imasring  14479  opprrng  14492  opprring  14494  mulgass3  14501  dvdsrtr  14518  dvdsrmul1  14519  unitgrp  14533  dvrass  14556  dvrcan1  14557  dvrcan3  14558  dvrdir  14560  rdivmuldivd  14561  rhmunitinv  14595  lringuplu  14613  subrginv  14655  unitrrg  14686  aprcotr  14707  islmod  14737  lmod0vs  14768  lmodvs0  14769  lmodvsmmulgdi  14770  lmodfopne  14773  lmodvneg1  14777  lmodvsneg  14778  lmodcom  14780  lmodsubvs  14790  lmodsubdi  14791  lmodsubdir  14792  islss3  14826  lss1d  14830  sralmod  14897  rnglidlmsgrp  14944  2idlcpblrng  14970  mulgrhm  15054  assa2ass  15119  assa2ass2  15120  asclghm  15135  asclmul1  15139  asclmul2  15140  ascldimul  15141  assamulgscmlem2  15152  asclmulg  15154  psrass1fi  15206  psrdifi  15207  psrdirfi  15208  psmetsym  15567  psmettri  15568  psmetge0  15569  psmetres2  15571  xmetge0  15603  xmetsym  15606  xmettri  15610  metrtri  15615  xmetres2  15617  bldisj  15639  xblss2ps  15642  xblss2  15643  xmeter  15674  xmetxp  15745  dvdsppwf1o  16295  perfect1  16310  perfectlem1  16311  perfectlem2  16312  3dom  17235