Theorem syl13anc 1240

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

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

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 980

This theorem is referenced by:  syl23anc  1245  syl33anc  1253  caovassd  6036  caovcand  6039  caovordid  6043  caovordd  6045  caovdid  6052  caovdird  6055  swoer  6565  swoord1  6566  swoord2  6567  fimax2gtrilemstep  6902  iunfidisj  6947  ssfii  6975  suplub2ti  7002  prarloclem3  7498  fzosubel3  10198  seq3split  10481  seq3caopr  10485  zsumdc  11394  fsumiun  11487  divalglemex  11929  pcgcd1  12329  strle1g  12567  mnd32g  12833  mnd12g  12834  mnd4g  12835  ismndd  12843  mndinvmod  12851  grpasscan2  12939  grpidrcan  12940  grpidlcan  12941  grpinvinv  12942  grplmulf1o  12949  grpinvssd  12952  grpinvadd  12953  grpsubrcan  12956  grpsubadd  12963  grpaddsubass  12965  grppncan  12966  grpsubsub4  12968  grppnpcan2  12969  grpnpncan  12970  grpnpncan0  12971  grpnnncan2  12972  dfgrp3mlem  12973  dfgrp3m  12974  grplactcnv  12977  mhmmnd  12985  mulgaddcomlem  13011  mulgaddcom  13012  mulgnn0dir  13018  mulgdirlem  13019  mulgneg2  13022  mulgnnass  13023  mulgnn0ass  13024  mulgass  13025  mulgmodid  13027  nsgconj  13071  isnsg3  13072  nmzsubg  13075  ssnmz  13076  eqger  13088  eqgcpbl  13092  abl32  13115  abladdsub4  13122  abladdsub  13123  ablpncan2  13124  ablsubsub  13126  srgass  13159  srgmulgass  13177  srgpcomp  13178  srgpcompp  13179  srgpcomppsc  13180  ringass  13204  ringadd2  13215  ringo2times  13216  ringcom  13219  ringlz  13227  ringrz  13228  ringnegl  13233  ringnegr  13234  ringmneg1  13235  ringmneg2  13236  ringsubdi  13238  ringsubdir  13239  mulgass2  13240  opprring  13254  mulgass3  13259  dvdsrtr  13275  dvdsrmul1  13276  unitgrp  13290  dvrass  13313  dvrcan1  13314  dvrcan3  13315  dvrdir  13317  rdivmuldivd  13318  lringuplu  13342  subrginv  13363  aprcotr  13380  islmod  13386  lmod0vs  13416  lmodvs0  13417  lmodvsmmulgdi  13418  lmodfopne  13421  lmodvneg1  13425  lmodvsneg  13426  lmodcom  13428  lmodsubvs  13438  lmodsubdi  13439  lmodsubdir  13440  islss3  13471  lss1d  13475  psmetsym  13868  psmettri  13869  psmetge0  13870  psmetres2  13872  xmetge0  13904  xmetsym  13907  xmettri  13911  metrtri  13916  xmetres2  13918  bldisj  13940  xblss2ps  13943  xblss2  13944  xmeter  13975  xmetxp  14046