Theorem syl13anc 1273

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 1201	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
6		syl13anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
7	1, 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:  syl23anc  1278  syl33anc  1286  caovassd  6177  caovcand  6180  caovordid  6184  caovordd  6186  caovdid  6193  caovdird  6196  swoer  6725  swoord1  6726  swoord2  6727  fimax2gtrilemstep  7085  iunfidisj  7139  ssfii  7167  suplub2ti  7194  prarloclem3  7710  fzosubel3  10434  seq3split  10743  seqsplitg  10744  seq3caopr  10750  seqcaoprg  10751  zsumdc  11938  fsumiun  12031  divalglemex  12476  pcgcd1  12894  strle1g  13182  prdssgrpd  13491  mnd32g  13503  mnd12g  13504  mnd4g  13505  ismndd  13513  mndinvmod  13521  prdsmndd  13524  imasmnd  13529  grpassd  13588  grpasscan2  13640  grpidrcan  13641  grpidlcan  13642  grpinvinv  13643  grplmulf1o  13650  grpinvssd  13653  grpinvadd  13654  grpsubrcan  13657  grpsubadd  13664  grpaddsubass  13666  grppncan  13667  grpsubsub4  13669  grppnpcan2  13670  grpnpncan  13671  grpnpncan0  13672  grpnnncan2  13673  dfgrp3mlem  13674  dfgrp3m  13675  grplactcnv  13678  imasgrp  13691  mhmmnd  13696  mulgaddcomlem  13725  mulgaddcom  13726  mulgnn0dir  13732  mulgdirlem  13733  mulgneg2  13736  mulgnnass  13737  mulgnn0ass  13738  mulgass  13739  mulgmodid  13741  nsgconj  13786  isnsg3  13787  nmzsubg  13790  ssnmz  13791  eqger  13804  eqgcpbl  13808  conjghm  13856  conjnmz  13859  conjnmzb  13860  abl32  13887  abladdsub4  13894  abladdsub  13895  ablpncan2  13896  ablsubsub  13898  rngass  13945  rnglz  13951  rngrz  13952  rngmneg1  13953  rngmneg2  13954  rngsubdi  13957  rngsubdir  13958  imasrng  13962  srgass  13977  srgmulgass  13995  srgpcomp  13996  srgpcompp  13997  srgpcomppsc  13998  ringass  14022  ringadd2  14033  ringo2times  14034  ringcom  14037  ringlz  14049  ringrz  14050  ringnegl  14057  ringnegr  14058  ringmneg1  14059  ringmneg2  14060  ringsubdi  14062  ringsubdir  14063  mulgass2  14064  imasring  14070  opprrng  14083  opprring  14085  mulgass3  14091  dvdsrtr  14108  dvdsrmul1  14109  unitgrp  14123  dvrass  14146  dvrcan1  14147  dvrcan3  14148  dvrdir  14150  rdivmuldivd  14151  rhmunitinv  14185  lringuplu  14203  subrginv  14244  unitrrg  14274  aprcotr  14292  islmod  14298  lmod0vs  14328  lmodvs0  14329  lmodvsmmulgdi  14330  lmodfopne  14333  lmodvneg1  14337  lmodvsneg  14338  lmodcom  14340  lmodsubvs  14350  lmodsubdi  14351  lmodsubdir  14352  islss3  14386  lss1d  14390  sralmod  14457  rnglidlmsgrp  14504  2idlcpblrng  14530  mulgrhm  14616  psmetsym  15046  psmettri  15047  psmetge0  15048  psmetres2  15050  xmetge0  15082  xmetsym  15085  xmettri  15089  metrtri  15094  xmetres2  15096  bldisj  15118  xblss2ps  15121  xblss2  15122  xmeter  15153  xmetxp  15224  dvdsppwf1o  15706  perfect1  15715  perfectlem1  15716  perfectlem2  15717  3dom  16537