Theorem syl13anc 1275

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

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

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 1006

This theorem is referenced by:  syl23anc  1280  syl33anc  1288  caovassd  6182  caovcand  6185  caovordid  6189  caovordd  6191  caovdid  6198  caovdird  6201  swoer  6730  swoord1  6731  swoord2  6732  fimax2gtrilemstep  7090  iunfidisj  7145  ssfii  7173  suplub2ti  7200  prarloclem3  7717  fzosubel3  10442  seq3split  10751  seqsplitg  10752  seq3caopr  10758  seqcaoprg  10759  zsumdc  11950  fsumiun  12043  divalglemex  12488  pcgcd1  12906  strle1g  13194  prdssgrpd  13503  mnd32g  13515  mnd12g  13516  mnd4g  13517  ismndd  13525  mndinvmod  13533  prdsmndd  13536  imasmnd  13541  grpassd  13600  grpasscan2  13652  grpidrcan  13653  grpidlcan  13654  grpinvinv  13655  grplmulf1o  13662  grpinvssd  13665  grpinvadd  13666  grpsubrcan  13669  grpsubadd  13676  grpaddsubass  13678  grppncan  13679  grpsubsub4  13681  grppnpcan2  13682  grpnpncan  13683  grpnpncan0  13684  grpnnncan2  13685  dfgrp3mlem  13686  dfgrp3m  13687  grplactcnv  13690  imasgrp  13703  mhmmnd  13708  mulgaddcomlem  13737  mulgaddcom  13738  mulgnn0dir  13744  mulgdirlem  13745  mulgneg2  13748  mulgnnass  13749  mulgnn0ass  13750  mulgass  13751  mulgmodid  13753  nsgconj  13798  isnsg3  13799  nmzsubg  13802  ssnmz  13803  eqger  13816  eqgcpbl  13820  conjghm  13868  conjnmz  13871  conjnmzb  13872  abl32  13899  abladdsub4  13906  abladdsub  13907  ablpncan2  13908  ablsubsub  13910  rngass  13958  rnglz  13964  rngrz  13965  rngmneg1  13966  rngmneg2  13967  rngsubdi  13970  rngsubdir  13971  imasrng  13975  srgass  13990  srgmulgass  14008  srgpcomp  14009  srgpcompp  14010  srgpcomppsc  14011  ringass  14035  ringadd2  14046  ringo2times  14047  ringcom  14050  ringlz  14062  ringrz  14063  ringnegl  14070  ringnegr  14071  ringmneg1  14072  ringmneg2  14073  ringsubdi  14075  ringsubdir  14076  mulgass2  14077  imasring  14083  opprrng  14096  opprring  14098  mulgass3  14104  dvdsrtr  14121  dvdsrmul1  14122  unitgrp  14136  dvrass  14159  dvrcan1  14160  dvrcan3  14161  dvrdir  14163  rdivmuldivd  14164  rhmunitinv  14198  lringuplu  14216  subrginv  14257  unitrrg  14287  aprcotr  14305  islmod  14311  lmod0vs  14341  lmodvs0  14342  lmodvsmmulgdi  14343  lmodfopne  14346  lmodvneg1  14350  lmodvsneg  14351  lmodcom  14353  lmodsubvs  14363  lmodsubdi  14364  lmodsubdir  14365  islss3  14399  lss1d  14403  sralmod  14470  rnglidlmsgrp  14517  2idlcpblrng  14543  mulgrhm  14629  psmetsym  15059  psmettri  15060  psmetge0  15061  psmetres2  15063  xmetge0  15095  xmetsym  15098  xmettri  15102  metrtri  15107  xmetres2  15109  bldisj  15131  xblss2ps  15134  xblss2  15135  xmeter  15166  xmetxp  15237  dvdsppwf1o  15719  perfect1  15728  perfectlem1  15729  perfectlem2  15730  3dom  16613