Theorem syl13anc 1252

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 1180	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 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:  syl23anc  1257  syl33anc  1265  caovassd  6116  caovcand  6119  caovordid  6123  caovordd  6125  caovdid  6132  caovdird  6135  swoer  6658  swoord1  6659  swoord2  6660  fimax2gtrilemstep  7009  iunfidisj  7060  ssfii  7088  suplub2ti  7115  prarloclem3  7623  fzosubel3  10338  seq3split  10646  seqsplitg  10647  seq3caopr  10653  seqcaoprg  10654  zsumdc  11745  fsumiun  11838  divalglemex  12283  pcgcd1  12701  strle1g  12988  prdssgrpd  13297  mnd32g  13309  mnd12g  13310  mnd4g  13311  ismndd  13319  mndinvmod  13327  prdsmndd  13330  imasmnd  13335  grpassd  13394  grpasscan2  13446  grpidrcan  13447  grpidlcan  13448  grpinvinv  13449  grplmulf1o  13456  grpinvssd  13459  grpinvadd  13460  grpsubrcan  13463  grpsubadd  13470  grpaddsubass  13472  grppncan  13473  grpsubsub4  13475  grppnpcan2  13476  grpnpncan  13477  grpnpncan0  13478  grpnnncan2  13479  dfgrp3mlem  13480  dfgrp3m  13481  grplactcnv  13484  imasgrp  13497  mhmmnd  13502  mulgaddcomlem  13531  mulgaddcom  13532  mulgnn0dir  13538  mulgdirlem  13539  mulgneg2  13542  mulgnnass  13543  mulgnn0ass  13544  mulgass  13545  mulgmodid  13547  nsgconj  13592  isnsg3  13593  nmzsubg  13596  ssnmz  13597  eqger  13610  eqgcpbl  13614  conjghm  13662  conjnmz  13665  conjnmzb  13666  abl32  13693  abladdsub4  13700  abladdsub  13701  ablpncan2  13702  ablsubsub  13704  rngass  13751  rnglz  13757  rngrz  13758  rngmneg1  13759  rngmneg2  13760  rngsubdi  13763  rngsubdir  13764  imasrng  13768  srgass  13783  srgmulgass  13801  srgpcomp  13802  srgpcompp  13803  srgpcomppsc  13804  ringass  13828  ringadd2  13839  ringo2times  13840  ringcom  13843  ringlz  13855  ringrz  13856  ringnegl  13863  ringnegr  13864  ringmneg1  13865  ringmneg2  13866  ringsubdi  13868  ringsubdir  13869  mulgass2  13870  imasring  13876  opprrng  13889  opprring  13891  mulgass3  13897  dvdsrtr  13913  dvdsrmul1  13914  unitgrp  13928  dvrass  13951  dvrcan1  13952  dvrcan3  13953  dvrdir  13955  rdivmuldivd  13956  rhmunitinv  13990  lringuplu  14008  subrginv  14049  unitrrg  14079  aprcotr  14097  islmod  14103  lmod0vs  14133  lmodvs0  14134  lmodvsmmulgdi  14135  lmodfopne  14138  lmodvneg1  14142  lmodvsneg  14143  lmodcom  14145  lmodsubvs  14155  lmodsubdi  14156  lmodsubdir  14157  islss3  14191  lss1d  14195  sralmod  14262  rnglidlmsgrp  14309  2idlcpblrng  14335  mulgrhm  14421  psmetsym  14851  psmettri  14852  psmetge0  14853  psmetres2  14855  xmetge0  14887  xmetsym  14890  xmettri  14894  metrtri  14899  xmetres2  14901  bldisj  14923  xblss2ps  14926  xblss2  14927  xmeter  14958  xmetxp  15029  dvdsppwf1o  15511  perfect1  15520  perfectlem1  15521  perfectlem2  15522