Theorem syl13anc 1251

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

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

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 982

This theorem is referenced by:  syl23anc  1256  syl33anc  1264  caovassd  6087  caovcand  6090  caovordid  6094  caovordd  6096  caovdid  6103  caovdird  6106  swoer  6629  swoord1  6630  swoord2  6631  fimax2gtrilemstep  6970  iunfidisj  7021  ssfii  7049  suplub2ti  7076  prarloclem3  7581  fzosubel3  10289  seq3split  10597  seqsplitg  10598  seq3caopr  10604  seqcaoprg  10605  zsumdc  11566  fsumiun  11659  divalglemex  12104  pcgcd1  12522  strle1g  12809  prdssgrpd  13117  mnd32g  13129  mnd12g  13130  mnd4g  13131  ismndd  13139  mndinvmod  13147  prdsmndd  13150  imasmnd  13155  grpassd  13214  grpasscan2  13266  grpidrcan  13267  grpidlcan  13268  grpinvinv  13269  grplmulf1o  13276  grpinvssd  13279  grpinvadd  13280  grpsubrcan  13283  grpsubadd  13290  grpaddsubass  13292  grppncan  13293  grpsubsub4  13295  grppnpcan2  13296  grpnpncan  13297  grpnpncan0  13298  grpnnncan2  13299  dfgrp3mlem  13300  dfgrp3m  13301  grplactcnv  13304  imasgrp  13317  mhmmnd  13322  mulgaddcomlem  13351  mulgaddcom  13352  mulgnn0dir  13358  mulgdirlem  13359  mulgneg2  13362  mulgnnass  13363  mulgnn0ass  13364  mulgass  13365  mulgmodid  13367  nsgconj  13412  isnsg3  13413  nmzsubg  13416  ssnmz  13417  eqger  13430  eqgcpbl  13434  conjghm  13482  conjnmz  13485  conjnmzb  13486  abl32  13513  abladdsub4  13520  abladdsub  13521  ablpncan2  13522  ablsubsub  13524  rngass  13571  rnglz  13577  rngrz  13578  rngmneg1  13579  rngmneg2  13580  rngsubdi  13583  rngsubdir  13584  imasrng  13588  srgass  13603  srgmulgass  13621  srgpcomp  13622  srgpcompp  13623  srgpcomppsc  13624  ringass  13648  ringadd2  13659  ringo2times  13660  ringcom  13663  ringlz  13675  ringrz  13676  ringnegl  13683  ringnegr  13684  ringmneg1  13685  ringmneg2  13686  ringsubdi  13688  ringsubdir  13689  mulgass2  13690  imasring  13696  opprrng  13709  opprring  13711  mulgass3  13717  dvdsrtr  13733  dvdsrmul1  13734  unitgrp  13748  dvrass  13771  dvrcan1  13772  dvrcan3  13773  dvrdir  13775  rdivmuldivd  13776  rhmunitinv  13810  lringuplu  13828  subrginv  13869  unitrrg  13899  aprcotr  13917  islmod  13923  lmod0vs  13953  lmodvs0  13954  lmodvsmmulgdi  13955  lmodfopne  13958  lmodvneg1  13962  lmodvsneg  13963  lmodcom  13965  lmodsubvs  13975  lmodsubdi  13976  lmodsubdir  13977  islss3  14011  lss1d  14015  sralmod  14082  rnglidlmsgrp  14129  2idlcpblrng  14155  mulgrhm  14241  psmetsym  14649  psmettri  14650  psmetge0  14651  psmetres2  14653  xmetge0  14685  xmetsym  14688  xmettri  14692  metrtri  14697  xmetres2  14699  bldisj  14721  xblss2ps  14724  xblss2  14725  xmeter  14756  xmetxp  14827  dvdsppwf1o  15309  perfect1  15318  perfectlem1  15319  perfectlem2  15320