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  6249  caovcand  6252  caovordid  6256  caovordd  6258  caovdid  6265  caovdird  6268  swoer  6835  swoord1  6836  swoord2  6837  fimax2gtrilemstep  7205  iunfidisj  7260  ssfii  7308  suplub2ti  7342  prarloclem3  7865  fzosubel3  10625  seq3split  10939  seqsplitg  10940  seq3caopr  10946  seqcaoprg  10947  zsumdc  12169  fsumiun  12262  divalglemex  12707  pcgcd1  13129  strle1g  13511  mnd32g  13791  mnd12g  13792  mnd4g  13793  ismndd  13801  mndinvmod  13809  imasmnd  13811  grpassd  13868  grpasscan2  13920  grpidrcan  13921  grpidlcan  13922  grpinvinv  13923  grplmulf1o  13930  grpinvssd  13933  grpinvadd  13934  grpsubrcan  13937  grpsubadd  13944  grpaddsubass  13946  grppncan  13947  grpsubsub4  13949  grppnpcan2  13950  grpnpncan  13951  grpnpncan0  13952  grpnnncan2  13953  dfgrp3mlem  13954  dfgrp3m  13955  grplactcnv  13958  imasgrp  13965  mhmmnd  13970  mulgaddcomlem  13999  mulgaddcom  14000  mulgnn0dir  14006  mulgdirlem  14007  mulgneg2  14010  mulgnnass  14011  mulgnn0ass  14012  mulgass  14013  mulgmodid  14015  nsgconj  14060  isnsg3  14061  nmzsubg  14064  ssnmz  14065  eqger  14078  eqgcpbl  14082  conjghm  14130  conjnmz  14133  conjnmzb  14134  abl32  14161  abladdsub4  14169  abladdsub  14170  ablpncan2  14171  ablsubsub  14173  prdssgrpd  14242  prdsmndd  14245  rngass  14289  rnglz  14295  rngrz  14296  rngmneg1  14297  rngmneg2  14298  rngsubdi  14301  rngsubdir  14302  imasrng  14306  srgass  14326  srgmulgass  14344  srgpcomp  14345  srgpcompp  14346  srgpcomppsc  14347  ringass  14371  ringadd2  14383  ringo2times  14384  ringcom  14387  ringlz  14399  ringrz  14400  ringnegl  14407  ringnegr  14408  ringmneg1  14409  ringmneg2  14410  ringsubdi  14412  ringsubdir  14413  mulgass2  14414  imasring  14420  opprrng  14433  opprring  14435  mulgass3  14442  dvdsrtr  14459  dvdsrmul1  14460  unitgrp  14474  dvrass  14497  dvrcan1  14498  dvrcan3  14499  dvrdir  14501  rdivmuldivd  14502  rhmunitinv  14536  lringuplu  14554  subrginv  14596  unitrrg  14627  aprcotr  14648  islmod  14678  lmod0vs  14709  lmodvs0  14710  lmodvsmmulgdi  14711  lmodfopne  14714  lmodvneg1  14718  lmodvsneg  14719  lmodcom  14721  lmodsubvs  14731  lmodsubdi  14732  lmodsubdir  14733  islss3  14767  lss1d  14771  sralmod  14838  rnglidlmsgrp  14885  2idlcpblrng  14911  mulgrhm  14995  assa2ass  15060  assa2ass2  15061  asclghm  15076  asclmul1  15080  asclmul2  15081  ascldimul  15082  assamulgscmlem2  15093  asclmulg  15095  psmetsym  15482  psmettri  15483  psmetge0  15484  psmetres2  15486  xmetge0  15518  xmetsym  15521  xmettri  15525  metrtri  15530  xmetres2  15532  bldisj  15554  xblss2ps  15557  xblss2  15558  xmeter  15589  xmetxp  15660  dvdsppwf1o  16205  perfect1  16220  perfectlem1  16221  perfectlem2  16222  3dom  17140