Theorem syl13anc 1276

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

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

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 1007

This theorem is referenced by:  syl23anc  1281  syl33anc  1289  caovassd  6222  caovcand  6225  caovordid  6229  caovordd  6231  caovdid  6238  caovdird  6241  swoer  6808  swoord1  6809  swoord2  6810  fimax2gtrilemstep  7171  iunfidisj  7226  ssfii  7274  suplub2ti  7305  prarloclem3  7828  fzosubel3  10566  seq3split  10877  seqsplitg  10878  seq3caopr  10884  seqcaoprg  10885  zsumdc  12099  fsumiun  12192  divalglemex  12637  pcgcd1  13055  strle1g  13407  mnd32g  13692  mnd12g  13693  mnd4g  13694  ismndd  13702  mndinvmod  13710  imasmnd  13712  grpassd  13771  grpasscan2  13823  grpidrcan  13824  grpidlcan  13825  grpinvinv  13826  grplmulf1o  13833  grpinvssd  13836  grpinvadd  13837  grpsubrcan  13840  grpsubadd  13847  grpaddsubass  13849  grppncan  13850  grpsubsub4  13852  grppnpcan2  13853  grpnpncan  13854  grpnpncan0  13855  grpnnncan2  13856  dfgrp3mlem  13857  dfgrp3m  13858  grplactcnv  13861  imasgrp  13868  mhmmnd  13873  mulgaddcomlem  13902  mulgaddcom  13903  mulgnn0dir  13909  mulgdirlem  13910  mulgneg2  13913  mulgnnass  13914  mulgnn0ass  13915  mulgass  13916  mulgmodid  13918  nsgconj  13963  isnsg3  13964  nmzsubg  13967  ssnmz  13968  eqger  13981  eqgcpbl  13985  conjghm  14033  conjnmz  14036  conjnmzb  14037  abl32  14064  abladdsub4  14071  abladdsub  14072  ablpncan2  14073  ablsubsub  14075  prdssgrpd  14137  prdsmndd  14140  rngass  14182  rnglz  14188  rngrz  14189  rngmneg1  14190  rngmneg2  14191  rngsubdi  14194  rngsubdir  14195  imasrng  14199  srgass  14218  srgmulgass  14236  srgpcomp  14237  srgpcompp  14238  srgpcomppsc  14239  ringass  14263  ringadd2  14274  ringo2times  14275  ringcom  14278  ringlz  14290  ringrz  14291  ringnegl  14298  ringnegr  14299  ringmneg1  14300  ringmneg2  14301  ringsubdi  14303  ringsubdir  14304  mulgass2  14305  imasring  14311  opprrng  14324  opprring  14326  mulgass3  14333  dvdsrtr  14350  dvdsrmul1  14351  unitgrp  14365  dvrass  14388  dvrcan1  14389  dvrcan3  14390  dvrdir  14392  rdivmuldivd  14393  rhmunitinv  14427  lringuplu  14445  subrginv  14487  unitrrg  14518  aprcotr  14539  islmod  14569  lmod0vs  14599  lmodvs0  14600  lmodvsmmulgdi  14601  lmodfopne  14604  lmodvneg1  14608  lmodvsneg  14609  lmodcom  14611  lmodsubvs  14621  lmodsubdi  14622  lmodsubdir  14623  islss3  14657  lss1d  14661  sralmod  14728  rnglidlmsgrp  14775  2idlcpblrng  14801  mulgrhm  14887  psmetsym  15324  psmettri  15325  psmetge0  15326  psmetres2  15328  xmetge0  15360  xmetsym  15363  xmettri  15367  metrtri  15372  xmetres2  15374  bldisj  15396  xblss2ps  15399  xblss2  15400  xmeter  15431  xmetxp  15502  dvdsppwf1o  15987  perfect1  15996  perfectlem1  15997  perfectlem2  15998  3dom  16902