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

Theorem sylbir 238
 Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
sylbir.1 (𝜓𝜑)
sylbir.2 (𝜓𝜒)
Assertion
Ref Expression
sylbir (𝜑𝜒)

Proof of Theorem sylbir
StepHypRef Expression
1 sylbir.1 . . 3 (𝜓𝜑)
21biimpri 231 . 2 (𝜑𝜓)
3 sylbir.2 . 2 (𝜓𝜒)
42, 3syl 17 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  3imtr3i  294  ex  416  3expa  1115  3ori  1421  nanass  1501  19.38  1840  19.35  1878  sbi2  2306  nfeqf2  2384  equsex  2429  sbi2ALT  2583  dfmoeu  2594  2mo  2710  axie2  2765  necon1bi  3015  necon1i  3020  r19.35  3296  sbhypf  3501  vtocl2OLD  3511  spc2ed  3551  reu6  3667  rabssrabd  4012  uneqin  4208  difin0ss  4285  inelcm  4375  falseral0  4420  raaan2  4425  difprsn1  4696  tppreqb  4701  n0snor2el  4727  unissint  4866  intminss  4868  iununi  4988  triin  5155  bm1.3ii  5174  eusv2nf  5265  reusv3i  5274  moabex  5320  copsex2g  5353  opelopabt  5388  eqrelrel  5638  opeliunxp2  5677  opelrn  5783  ssxpb  6002  xpima  6010  xpimasn  6013  dmsn0el  6039  relcnvtr  6094  relcoi2  6103  elsnxp  6117  reuop  6119  iotanul  6310  dffv2  6743  fnfvrnss  6871  fressnfv  6909  fconst5  6955  f1mpt  7007  isocnv3  7074  f1owe  7095  ovprc  7183  fvmpopr2d  7301  onminesb  7506  onminsb  7507  onintrab  7509  onnminsb  7512  onsucuni2  7542  tfindsg2  7569  zfrep6  7651  fo1stres  7710  fo2ndres  7711  bropopvvv  7781  bropfvvvv  7783  frxp  7816  opeliunxp2f  7877  mpoxopoveqd  7888  reldmtpos  7901  wfrlem4  7959  wfrlem12  7967  wfrlem16  7971  wfr2  7975  tfrlem5  8017  tfrlem9  8022  tfr2  8035  rdgsuc  8061  oaordi  8173  oeordi  8214  omopthi  8285  fvmptmap  8446  mptelixpg  8500  ener  8557  domtr  8563  snfi  8595  unen  8597  xpf1o  8681  mapen  8683  unxpdomlem3  8726  isinf  8733  frfi  8765  unblem1  8772  unfi  8787  fofinf1o  8801  fsuppun  8854  inf3lem2  9094  inf3lem5  9097  cantnfp1lem1  9143  cantnfp1lem3  9145  tcmin  9185  r1ordg  9209  r1ord  9211  rankr1ai  9229  r1val3  9269  bndrank  9272  unbndrank  9273  rankr1b  9295  rankxplim3  9312  tcrank  9315  xpnum  9382  cardmin2  9430  infxpenlem  9442  fseqen  9456  dfac8clem  9461  alephsson  9529  alephfp  9537  dfac4  9551  kmlem6  9584  kmlem8  9586  kmlem9  9587  infpssr  9737  fin1a2lem12  9840  axcc4  9868  axcc4dom  9870  ac6s2  9915  zornn0g  9934  cardidg  9977  unsnen  9982  pwcfsdom  10012  cfpwsdom  10013  gchpwdom  10099  r1tskina  10211  intgru  10243  indpi  10336  nqereu  10358  supsrlem  10540  letrii  10772  dfnn3  11657  zaddcl  12030  nn0ind  12085  fnn0ind  12089  ublbneg  12341  nn01to3  12349  infmrp1  12745  fz0  12937  fzo1fzo0n0  13103  elfzom1elp1fzo  13119  fzo0end  13144  elfznelfzo  13157  fzind2  13170  injresinjlem  13172  fleqceilz  13237  nnsinds  13371  nn0sinds  13372  faclbnd4lem1  13669  hashinf  13711  hasheqf1oi  13728  hashgt0elex  13778  hashgt23el  13801  hashfacen  13828  hash2prde  13844  hash2sspr  13862  fun2dmnop0  13868  iswrddm0  13901  swrdnnn0nd  14029  swrdnd0  14030  swrdlsw  14040  pfxn0  14059  pfxnd0  14061  swrdswrdlem  14077  pfxccatin12lem3  14105  pfxccat3  14107  pfxccat3a  14111  swrdccat3blem  14112  cshwsublen  14169  cshwidxmod  14176  repswcshw  14185  cshw1  14195  trclun  14385  dmtrclfv  14389  rediv  14502  imdiv  14509  sqrt0  14613  fsump1i  15136  modfsummods  15160  bpolydiflem  15420  bpoly3  15424  bpoly4  15425  cos1bnd  15552  sinltx  15554  rpnnen2lem1  15579  rpnnen2lem2  15580  rpnnen2lem12  15590  odd2np1  15702  opoe  15724  omoe  15725  opeo  15726  omeo  15727  gcdcllem1  15858  gcdaddmlem  15882  dfgcd2  15904  algfx  15934  lcmledvds  15953  lcmfunsnlem  15995  lcmfun  15999  coprmprod  16015  coprmproddvdslem  16016  odzval  16138  odzdvds  16142  prmreclem5  16266  mul4sq  16300  prmgaplem5  16401  prmgaplem6  16402  imasaddfnlem  16813  mreexexlem4d  16930  joindmss  17629  meetdmss  17643  gictr  18428  cntzval  18464  symg2bas  18534  odfval  18673  efgsfo  18878  efgrelexlemb  18889  dprddomcld  19137  dprdsubg  19160  dprd2da  19178  lssacs  19753  cnfldinv  20143  ocvval  20378  selvval  20827  dmatmul  21143  mdetfval1  21236  mndifsplit  21282  fvmptnn04if  21495  toprntopon  21571  opnnei  21766  ordtbas2  21837  ordtrest2lem  21849  lmmo  22026  fincmp  22039  bwth  22056  txbas  22213  ptcnplem  22267  tx2ndc  22297  hmphtr  22429  fbun  22486  filconn  22529  ptcmplem5  22702  cnextcn  22713  utoptop  22881  ucncn  22932  metust  23206  cfilucfil  23207  elcncf1di  23541  xrhmeo  23592  phtpycc  23637  copco  23664  pcohtpylem  23665  pcopt  23668  pcopt2  23669  ncvsi  23797  ovolval  24118  iunmbl2  24202  itg2splitlem  24393  cpnfval  24576  plyval  24834  fta1  24948  aaliou2b  24981  tayl0  25001  ulmdvlem3  25041  radcnvlem2  25053  dvradcnv  25060  reeff1o  25086  sincosq1lem  25134  sincosq2sgn  25136  sincosq4sgn  25138  sinq12ge0  25145  logrncl  25203  eflog  25212  cxpge0  25318  logb1  25399  atanf  25510  atanbnd  25556  igamf  25680  igamcl  25681  lgsne0  25963  mul2sq  26047  2sqreultblem  26076  pntibnd  26221  ostth  26267  mptelee  26733  axlowdimlem9  26788  axlowdimlem12  26791  axcontlem2  26803  axcontlem12  26813  structgrssvtx  26861  structgrssiedg  26862  lpvtx  26905  nbuhgr  27177  nbumgr  27181  nbuhgr2vtx1edgblem  27185  nbgr0vtxlem  27189  nbgr1vtx  27192  uvtx01vtx  27231  prcliscplgr  27248  cusgrsizeinds  27286  sizusglecusglem2  27296  uhgrvd00  27368  fusgrregdegfi  27403  rusgr1vtxlem  27421  wlkeq  27467  wlk1walk  27472  uspgr2wlkeq  27479  wlklenvclwlk  27488  wlklenvclwlkOLD  27489  wlkreslem  27503  wlkdlem2  27517  wlkdlem4  27519  spthonepeq  27585  clwlkclwwlkflem  27833  clwlkclwwlkfolem  27836  clwlkclwwlkf  27837  clwwisshclwws  27844  clwwlkneq0  27858  3wlkdlem6  27994  eupth2eucrct  28046  eupth2lem1  28047  eupth2lem3lem7  28063  frgr3vlem1  28102  frgr3vlem2  28103  frgrncvvdeqlem8  28135  frgrncvvdeqlem9  28136  numclwwlk5  28217  frgrreg  28223  frgrregord013  28224  friendshipgt3  28227  isgrpo  28324  vciOLD  28388  vcex  28405  nmogtmnf  28597  siilem1  28678  siii  28680  ajmoi  28685  bcsiALT  29006  hhcms  29030  ocval  29107  hsupval  29161  omlsilem  29229  h1de2bi  29381  h1de2ctlem  29382  hosubeq0i  29653  adjmo  29659  nmopgtmnf  29695  nlfnval  29708  nmcopex  29856  nmcfnex  29880  riesz4i  29890  riesz1  29892  riesz2  29893  opsqrlem1  29967  superpos  30181  hatomistici  30189  chpssati  30190  mdsymlem3  30232  3o1cs  30277  3o2cs  30278  3o3cs  30279  iunrnmptss  30373  brabgaf  30416  f1mptrn  30438  ffsrn  30535  fpwrelmap  30539  xnn0gt0  30564  hashxpe  30599  prmidl2  31085  mxidlnzrb  31113  fedgmul  31181  ordtrest2NEWlem  31341  qqhval2  31399  esumfsup  31505  esumcvg  31521  cntnevol  31663  ddemeas  31671  dya2icoseg2  31712  dya2iocnei  31716  eulerpartlems  31794  eulerpartlemgvv  31810  eulerpart  31816  cndprobprob  31872  ballotlemsdom  31945  ballotth  31971  sgn3da  31975  bnj945  32221  bnj1379  32278  bnj1459  32291  bnj557  32349  bnj571  32354  bnj849  32373  bnj964  32391  bnj978  32397  bnj1018g  32411  bnj1018  32412  bnj1020  32413  bnj1033  32417  bnj1175  32452  bnj1398  32482  bnj1417  32489  bnj1523  32519  nummin  32540  cusgr3cyclex  32562  txpconn  32658  satfv1  32789  satffun  32835  msubco  32957  mclsax  32995  setinds  33206  dfon2lem7  33217  dfon2lem8  33218  poseq  33278  soseq  33279  frrlem4  33309  frr2  33328  nocvxminlem  33459  nocvxmin  33460  pprodss4v  33605  fullfunfv  33668  altxpsspw  33698  funtransport  33752  fvtransport  33753  funray  33861  fvray  33862  funline  33863  fvline  33865  finminlem  33926  bisym1  34027  onsucconni  34045  onsucsuccmpi  34051  bj-currypara  34159  bj-alcomexcom  34278  axc11n11r  34281  bj-equsal2  34414  bj-xpima1snALT  34544  bj-bm1.3ii  34632  bj-opelidb1ALT  34732  mptsnunlem  34906  iooelexlt  34930  relowlpssretop  34932  rdgeqoa  34938  difunieq  34942  nlpineqsn  34976  fvineqsneq  34980  wl-lem-nexmo  35119  matunitlindflem1  35204  ptrecube  35208  poimirlem26  35234  poimirlem30  35238  poimir  35241  ismblfin  35249  itg2addnclem  35259  dvasin  35292  sdclem2  35331  totbndbnd  35378  ismgmOLD  35439  exidresid  35468  isrngo  35486  rngoablo2  35498  rngoueqz  35529  isdivrngo  35539  isdrngo1  35545  isdrngo2  35547  ispridl2  35627  relcnveq3  35889  elrelscnveq3  36042  ax12eq  36388  ax12el  36389  lkr0f  36541  hl2at  36852  dalemswapyz  37103  pclfinclN  37397  osumcllem11N  37413  pexmidlem8N  37424  ltrnnid  37583  sn-00id  39710  mptfcl  39832  fphpd  39928  elmnc  40251  itgoval  40276  arearect  40336  reabsifpos  40505  clsk3nimkb  40914  grumnud  41165  nanorxor  41180  pm11.71  41272  iotavalsb  41308  sbiota1  41309  2uasbanh  41438  eel0TT  41581  eelT00  41582  eelTTT  41583  eelT11  41584  eelT12  41586  eelTT1  41587  eelT01  41588  eel0T1  41589  eelTT  41648  uunT1p1  41658  uun121  41660  uun121p1  41661  un2122  41667  uunTT1  41670  uunTT1p1  41671  uunTT1p2  41672  uunT11  41673  uunT11p1  41674  uunT11p2  41675  uunT12  41676  uunT12p1  41677  uunT12p2  41678  uunT12p3  41679  uunT12p4  41680  uunT12p5  41681  uun111  41682  3anidm12p2  41684  uun123  41685  3impdirp1  41693  undif3VD  41759  ax6e2ndeqVD  41786  2uasbanhVD  41788  ax6e2ndeqALT  41808  iunconnlem2  41812  sineq0ALT  41814  ioodvbdlimc1lem2  42742  ioodvbdlimc2lem  42744  stoweidlem3  42813  stoweidlem17  42827  fourierdlem42  42959  fourierdlem48  42964  fourierdlem50  42966  fourierdlem51  42967  fourierdlem76  42992  fourierdlem83  42999  fourierdlem87  43003  hoidmvval0  43394  rexrsb  43823  2reu8i  43837  2reuimp  43839  afv0nbfvbi  43875  afvfv0bi  43876  afveu  43877  fnbrafvb  43878  afvres  43896  tz6.12-afv  43897  dmfcoafv  43899  afvco2  43900  aovprc  43912  aovrcl  43913  aovmpt4g  43925  afv2eu  43962  afv2res  43963  tz6.12-afv2  43964  tz6.12i-afv2  43967  afv2rnfveq  43986  fvmptrab  44016  fvmptrabdm  44017  fzopred  44047  2ffzoeq  44053  elsprel  44160  prproropf1o  44192  reupr  44207  lighneal  44297  odd2prm2  44404  even3prm2  44405  upgrwlkupwlk  44536  ovn0ssdmfun  44555  islinindfis  45024  rrx2linest  45322  line2ylem  45331  setrec2fun  45388  elsetrecslem  45394  setrecsres  45397  secval  45439  cscval  45440  cotval  45441
 Copyright terms: Public domain W3C validator