MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl122anc Structured version   Visualization version   GIF version

Theorem syl122anc 1486
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl122anc.6 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl122anc (𝜑𝜁)

Proof of Theorem syl122anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 555 . 2 (𝜑 → (𝜏𝜂))
7 syl122anc.6 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂)) → 𝜁)
81, 2, 3, 6, 7syl121anc 1482 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  divdiv32d  11018  divcan5d  11019  divcan7d  11021  divdiv1d  11024  divdiv2d  11025  seqcoll  13440  cau3lem  14293  eqsqrtd  14306  isercolllem2  14595  isercoll  14597  summolem2a  14645  divrcnv  14783  prodmolem2a  14863  prmind2  15600  divnumden  15658  pceulem  15752  pcqmul  15760  pcqdiv  15764  pcexp  15766  pcaddlem  15794  pcbc  15806  prmodvdslcmf  15953  latledi  17290  latjjdi  17304  latjjdir  17305  sylow1lem1  18213  sylow1lem5  18217  efgred2  18366  abladdsub4  18419  ablpnpcan  18425  ghmplusg  18449  frgpnabllem2  18477  isabvd  19022  lmodvs1  19093  lspsolvlem  19344  evlslem1  19717  frgpcyg  20124  ip2di  20188  mdetuni0  20629  cpmadugsumlemB  20881  elptr2  21579  blss2ps  22409  blss2  22410  blssps  22430  blss  22431  xmeter  22439  metdcnlem  22840  lebnumii  22966  minveclem2  23397  pjthlem1  23408  volfiniun  23515  dvfsumrlimge0  23992  lgsdi  25258  ax5seglem3  26010  ax5seglem6  26013  axcontlem8  26050  eengtrkg  26064  vacn  27858  minvecolem2  28040  minvecolem4  28045  disjabrex  29702  disjabrexf  29703  slmdvs1  30082  slmd0vs  30086  orngsqr  30113  ornglmulle  30114  orngrmulle  30115  orngmullt  30118  suborng  30124  madjusmdetlem1  30202  cgrcomand  32404  cgrcomr  32410  cgrcomland  32412  cgrcomrand  32413  cgrtriv  32415  cgrid2  32416  ofscom  32420  cgrextend  32421  segconeq  32423  btwntriv2  32425  btwnexch3and  32434  btwnouttr2  32435  btwnouttr  32437  btwnexch  32438  btwnexchand  32439  btwndiff  32440  ifscgr  32457  cgrsub  32458  cgrxfr  32468  lineext  32489  endofsegid  32498  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem4  32503  btwnconn1lem5  32504  btwnconn1lem7  32506  btwnconn1lem8  32507  btwnconn1lem10  32509  btwnconn1lem11  32510  btwnconn1lem13  32512  btwnconn1lem14  32513  btwnconn3  32516  midofsegid  32517  segcon2  32518  brsegle2  32522  seglecgr12im  32523  seglecgr12  32524  seglerflx  32525  seglemin  32526  segletr  32527  btwnsegle  32530  colinbtwnle  32531  btwnoutside  32538  broutsideof3  32539  outsideoftr  32542  outsideofeq  32543  outsidele  32545  lineunray  32560  lineelsb2  32561  lfladdcl  34861  lshpkrlem4  34903  latmmdiN  35024  latmmdir  35025  hlatj4  35163  4atlem4b  35389  4atlem11  35398  4atlem12  35401  dalem2  35450  dalem-cly  35460  dalem10  35462  dalem23  35485  dalem38  35499  dalem44  35505  dalem55  35516  cdlema1N  35580  paddclN  35631  pmapjoin  35641  dalawlem3  35662  dalawlem5  35664  dalawlem7  35666  dalawlem8  35667  dalawlem11  35670  dalawlem12  35671  lhpexle3lem  35800  4atexlemc  35858  trlnidat  35963  arglem1N  35980  cdlemd9  35996  cdleme0moN  36015  cdleme11c  36051  cdleme11h  36056  cdleme11  36060  cdleme16c  36070  cdleme16f  36073  cdlemeda  36088  cdleme20l2  36111  cdlemefs32sn1aw  36204  cdleme43fsv1snlem  36210  cdleme41sn3a  36223  cdleme32fva  36227  cdleme32b  36232  cdleme32c  36233  cdleme32e  36235  cdleme40m  36257  cdleme40n  36258  cdleme42e  36269  cdleme48d  36325  cdlemf2  36352  cdlemf  36353  cdlemg2fv2  36390  cdlemg7fvbwN  36397  cdlemg7fvN  36414  cdlemg9a  36422  cdlemg9b  36423  cdlemg10a  36430  cdlemg12b  36434  cdlemg17b  36452  cdlemg31d  36490  cdlemg33b0  36491  cdlemg33a  36496  ltrnco  36509  ltrncom  36528  cdlemh  36607  cdlemk3  36623  cdlemk12  36640  cdlemk12u  36662  cdlemkfid1N  36711  cdlemk51  36743  cdlemk54  36748  cdlemk43N  36753  cdlemk35u  36754  cdlemk55u1  36755  cdlemk39u1  36757  cdlemk19u1  36759  dia2dimlem10  36864  dvhgrp  36898  dvh0g  36902  cdlemm10N  36909  diblsmopel  36962  cdlemn4  36989  cdlemn6  36993  cdlemn7  36994  dihordlem7  37005  dihord1  37009  dihord2pre  37016  dihvalcqat  37030  dihopelvalcpre  37039  dihord5apre  37053  dihord  37055  dih1  37077  dihglbcpreN  37091  dihjatc1  37102  dihmeetlem13N  37110  dihmeetALTN  37118  dihjatcclem1  37209  baerlem3lem1  37498  pellfundex  37952  rmxypairf1o  37978  rmxycomplete  37984  rmxyneg  37987  rmxyadd  37988  rmxy1  37989  rmxy0  37990  jm2.22  38064  proot1mul  38279  deg1mhm  38287  stoweidlem7  40727  stoweidlem36  40756
  Copyright terms: Public domain W3C validator