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

Theorem bitr4d 283
Description: Deduction form of bitr4i 279. (Contributed by NM, 30-Jun-1993.)
Hypotheses
Ref Expression
bitr4d.1 (𝜑 → (𝜓𝜒))
bitr4d.2 (𝜑 → (𝜃𝜒))
Assertion
Ref Expression
bitr4d (𝜑 → (𝜓𝜃))

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2 (𝜑 → (𝜓𝜒))
2 bitr4d.2 . . 3 (𝜑 → (𝜃𝜒))
32bicomd 224 . 2 (𝜑 → (𝜒𝜃))
41, 3bitrd 280 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3bitr2d  308  3bitr2rd  309  3bitr4d  312  3bitr4rd  313  bianabs  542  mpbirand  703  sb3b  2494  sbcom3  2541  sbal1  2565  sbal2  2566  sbal2OLD  2567  2reu4lem  4461  issn  4755  disjprgw  5052  disjprg  5053  reuhypd  5310  ordtri3  6220  ordsssuc  6270  iota1  6325  funbrfv2b  6716  dffn5  6717  feqmptdf  6728  unima  6732  dmfco  6750  fneqeql  6808  f1ompt  6867  dff13  7004  fliftcnv  7053  soisores  7069  isotr  7078  isoini  7080  caovord3  7350  releldm2  7731  fimaproj  7818  brtpos  7890  tpostpos  7901  oe1m  8160  oawordri  8165  oalimcl  8175  omlimcl  8193  omabs  8263  iserd  8304  qliftel  8369  qliftfun  8371  qliftf  8374  ecopovsym  8388  pw2f1olem  8609  mapen  8669  suppeqfsuppbi  8835  mapfien  8859  supisolem  8925  cantnflem1  9140  wemapwe  9148  rankr1clem  9237  rankr1c  9238  ranklim  9261  r1pwALT  9263  r1pwcl  9264  isfin1-2  9795  isfin1-4  9797  fin71num  9807  axdc3lem2  9861  ltmnq  10382  prlem936  10457  ltsosr  10504  ltasr  10510  xrlenlt  10694  ltxrlt  10699  letri3  10714  ne0gt0  10733  subadd  10877  ltsubadd2  11099  lesubadd2  11101  suble  11106  ltsub23  11108  ltaddpos2  11119  ltsubpos  11120  subge02  11144  ltord2  11157  leord2  11158  ltaddsublt  11255  divmul  11289  divmul3  11291  rec11r  11327  ltdiv1  11492  ltdivmul2  11505  ledivmul2  11507  ltrec  11510  ltdiv2  11514  negfi  11577  negiso  11609  nnle1eq1  11655  avgle1  11865  avgle2  11866  avgle  11867  nn0le0eq0  11913  elz2  11987  znnnlt1  11997  zleltp1  12021  difrp  12415  xrltlen  12527  dfle2  12528  xrletri3  12535  xgepnf  12546  xlemnf  12548  qbtwnre  12580  xltnegi  12597  supxrre  12708  infxrre  12717  elioo5  12782  elfz5  12888  elfzm11  12966  predfz  13020  flbi  13174  flbi2  13175  fldiv4lem1div2uz2  13194  fznnfl  13218  zmodid2  13255  2submod  13288  lt2sq  13486  le2sq  13487  sqlecan  13559  bcval5  13666  pfxsuffeqwrdeq  14048  shftfib  14419  mulre  14468  cnpart  14587  sqrlem6  14595  sqrmo  14599  elicc4abs  14667  abs2difabs  14682  cau4  14704  limsupgre  14826  clim2  14849  ello1mpt2  14867  lo1resb  14909  o1resb  14911  climeq  14912  climmpt2  14918  isercoll  15012  caucvgb  15024  fsumabs  15144  isumshft  15182  geomulcvg  15220  absefib  15539  dvdsval3  15599  dvdsabseq  15651  dvdsflip  15655  dvdsssfz1  15656  mod2eq1n2dvds  15684  ndvdsadd  15749  bitscmp  15775  smupvallem  15820  dvdssq  15899  lcmdvds  15940  ncoprmgcdgt1b  15983  isprm3  16015  isprm5  16039  phiprmpw  16101  prmdiv  16110  pc11  16204  pcz  16205  pockthlem  16229  prmreclem2  16241  prmreclem4  16243  prmreclem6  16245  1arith  16251  vdwapun  16298  rami  16339  ramcl  16353  pwsle  16753  ercpbllem  16809  invsym  17020  funcres2c  17159  latnle  17683  grpinvcnv  18105  subgacs  18251  eqger  18268  gexdvds2  18639  pgpfi1  18649  pgpfi  18659  lsmass  18724  lssnle  18729  lsmdisj3b  18745  lsmhash  18760  ablsubadd  18861  gsumval3lem2  18955  subgdmdprd  19085  pgpfac1lem2  19126  dvdsr02  19335  drngid2  19447  issubrg3  19492  sdrgacs  19509  lssacs  19668  psrbaglefi  20080  coe1mul2lem1  20363  prmirred  20570  chrdvds  20603  chrcong  20604  chrnzr  20605  znleval  20629  znleval2  20630  cygznlem3  20644  frlmbas  20827  elfilspd  20875  lindfmm  20899  islindf4  20910  islindf5  20911  mdetunilem9  21157  isneip  21641  neiptopnei  21668  lpdifsn  21679  restopnb  21711  restopn2  21713  restdis  21714  restperf  21720  lmbr2  21795  cncls2  21809  cnprest  21825  cnprest2  21826  iscnrm2  21874  ist0-2  21880  ist1-3  21885  ishaus2  21887  cmpfi  21944  dfconn2  21955  1stccnp  21998  subislly  22017  hausmapdom  22036  tx1cn  22145  tx2cn  22146  txcnmpt  22160  txrest  22167  hauseqlcld  22182  tgqtop  22248  qtopcld  22249  ordthmeolem  22337  trfil2  22423  trfil3  22424  trnei  22428  ufildr  22467  fmfg  22485  rnelfm  22489  fmfnfm  22494  elflim  22507  flimrest  22519  cnflf  22538  cnflf2  22539  ptcmplem2  22589  ghmcnp  22650  tsmssubm  22678  iscfilu  22824  xmetgt0  22895  prdsxmetlem  22905  blcomps  22930  blcom  22931  xblpnfps  22932  xblpnf  22933  blpnf  22934  xmeter  22970  setsxms  23016  imasf1obl  23025  stdbdbl  23054  metrest  23061  metuel2  23102  dscopn  23110  xrtgioo  23341  metdstri  23386  cnmpopc  23459  iihalf2  23464  icopnfhmeo  23474  evth2  23491  lmmbr3  23790  iscau3  23808  metcld  23836  cfilucfil3  23850  srabn  23890  rrxmet  23938  minveclem4  23962  evthicc2  23988  ovolgelb  24008  shft2rab  24036  ovolshftlem1  24037  sca2rab  24040  ovolscalem1  24041  ioombl1lem4  24089  mbfmulc2lem  24175  ismbf3d  24182  mbfsup  24192  mbfinf  24193  i1f1lem  24217  i1fmulclem  24230  mbfi1fseqlem4  24246  itg2seq  24270  ditgneg  24382  limcdif  24401  limcnlp  24403  cnplimc  24412  rolle  24514  mvth  24516  dvne0  24535  lhop1lem  24537  itgsubst  24573  mdegle0  24598  deg1leb  24616  deg1le0  24632  q1peqb  24675  coemulhi  24771  dgrlt  24783  plydivlem3  24811  vieta1lem2  24827  aannenlem1  24844  ulmres  24903  reefiso  24963  pilem3  24968  ellogdm  25149  root1eq1  25263  angpieqvdlem  25333  angpieqvdlem2  25334  quad2  25344  1cubr  25347  quart  25366  rlimcnp  25470  wilthlem2  25573  isppw  25618  dvdsflsumcom  25692  fsumvma  25716  logfac2  25720  chpchtsum  25722  dchrmulcl  25752  dchrresb  25762  bclbnd  25783  bposlem1  25787  bposlem5  25791  gausslemma2dlem0c  25861  lgsquadlem1  25883  m1lgs  25891  2lgsoddprmlem2  25912  dchrisumlem3  25994  dchrisum0lem1  26019  tgjustr  26187  trgcgrg  26228  lnrot1  26336  islnopp  26452  ismidb  26491  islmib  26500  axsegconlem6  26635  axeuclidlem  26675  axcontlem2  26678  axcontlem4  26680  axcontlem12  26688  ausgrusgrb  26877  nb3grpr2  27092  cplgr2v  27141  umgr2v2enb1  27235  crctcsh  27529  clwwlknonwwlknonb  27812  eupth2lems  27944  nmoreltpnf  28473  isblo2  28487  nmlnogt0  28501  phoeqi  28561  ubthlem2  28575  hire  28798  normgt0  28831  ho01i  29532  ho02i  29533  hoeq1  29534  hoeq2  29535  nmopreltpnf  29573  adjeq  29639  leop  29827  leopmul2i  29839  pjnormssi  29872  pjimai  29880  jplem1  29972  mddmd2  30013  mdslmd1lem1  30029  mdslmd1lem2  30030  superpos  30058  atnssm0  30080  dmdbr5ati  30126  disjunsn  30272  fcoinvbr  30286  ofpreima  30338  funcnv5mpt  30341  isoun  30363  fpwrelmapffslem  30394  fpwrelmap  30395  iocinioc2  30428  xrdifh  30429  nndiffz1  30435  xdivmul  30528  cntzsnid  30623  isarchi2  30741  finexttrb  30951  smatrcl  30960  sqsscirc2  31051  xrmulc1cn  31072  esumfsup  31228  1stmbfm  31417  2ndmbfm  31418  mbfmcnt  31425  eulerpartlems  31517  eulerpartlemd  31523  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemsima  31672  ballotlemfrcn0  31686  sgn3da  31698  reprinfz1  31792  reprdifc  31797  bnj1173  32171  zltp1ne  32245  lfuhgr2  32262  erdszelem7  32341  erdszelem9  32343  iscvm  32403  cvmlift3lem4  32466  sltval2  33060  noextenddif  33072  sleloe  33130  sletri3  33131  fscgr  33438  seglelin  33474  btwnoutside  33483  lineunray  33505  cldbnd  33571  isfne4  33585  fneval  33597  filnetlem4  33626  nndivsub  33702  dfgcd3  34487  fvineqsneu  34574  wl-sbhbt  34671  wl-sbcom2d  34678  wl-sbalnae  34679  wl-ax11-lem8  34705  wl-dfrmof  34736  sin2h  34763  cos2h  34764  matunitlindflem1  34769  matunitlindflem2  34770  matunitlindf  34771  ptrest  34772  poimirlem3  34776  poimirlem4  34777  poimirlem22  34795  poimirlem27  34800  mblfinlem3  34812  mblfinlem4  34813  ismblfin  34814  itg2addnclem  34824  itg2addnclem2  34825  itg2gt0cn  34828  iblabsnclem  34836  ftc1anclem6  34853  areacirclem2  34864  areacirclem5  34867  areacirc  34868  mettrifi  34913  drngoi  35110  eldm4  35412  exanres2  35435  brcoss2  35557  br1cossres2  35565  eldmcoss2  35579  eldm1cossres2  35581  brcosscnv2  35593  erim2  35791  prter3  35898  islshpat  36033  lsatnle  36060  ellkr2  36107  lshpkr  36133  lkr0f2  36177  lduallkr3  36178  lkreqN  36186  cvrval2  36290  isat3  36323  glbconN  36393  hlrelat5N  36417  cvrval4N  36430  atlt  36453  1cvrco  36488  pmaple  36777  isline2  36790  isline4N  36793  elpaddn0  36816  elpadd2at2  36823  cdlemkid4  37950  dia0  38068  cdlemm10N  38134  dibglbN  38182  dihmeetlem4preN  38322  dochkrshp3  38404  dvh4dimlem  38459  lcfl5  38512  mapdpglem3  38691  mapdheq  38744  hdmap1eq  38817  hdmapval2lem  38847  hdmapoc  38947  hlhillcs  38974  renegadd  39080  resubadd  39087  fz1eqin  39244  diophin  39247  jm2.19  39468  rmxdiophlem  39490  pw2f1ocnv  39512  wepwsolem  39520  gicabl  39577  idomodle  39674  isdomn3  39682  ntrclsfveq2  40289  ntrclsss  40291  ntrclsk4  40300  extoimad  40393  radcnvrat  40523  bcc0  40549  supxrre3rnmpt  41579  clim2f  41793  clim2f2  41827  liminfreuzlem  41959  liminfltlem  41961  xlimmnflimsup2  42009  xlimpnfliminf2  42018  xlimlimsupleliminf  42020  opprb  43143  funbrafv2b  43235  dfafn5a  43236  leaddsuble  43374  iccpartgtprec  43457  flsqrt  43633  dfeven2  43691  dfodd3  43692  lindslinindimp2lem4  44444  snlindsntor  44454  regt1loggt0  44524  elbigo2  44540  elbigolo1  44545  fldivexpfllog2  44553  nnlog2ge0lt1  44554  blenpw2m1  44567
  Copyright terms: Public domain W3C validator