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  2499  sbcom3  2546  sbal1  2569  sbal2  2570  sbal2OLD  2571  2reu4lem  4467  issn  4761  disjprgw  5057  disjprg  5058  reuhypd  5315  ordtri3  6224  ordsssuc  6274  iota1  6329  funbrfv2b  6719  dffn5  6720  feqmptdf  6731  unima  6735  dmfco  6753  fneqeql  6811  f1ompt  6870  dff13  7010  fliftcnv  7059  soisores  7075  isotr  7084  isoini  7086  caovord3  7354  releldm2  7736  fimaproj  7823  brtpos  7895  tpostpos  7906  oe1m  8164  oawordri  8169  oalimcl  8179  omlimcl  8197  omabs  8267  iserd  8308  qliftel  8373  qliftfun  8375  qliftf  8378  ecopovsym  8392  pw2f1olem  8613  mapen  8673  suppeqfsuppbi  8839  mapfien  8863  supisolem  8929  cantnflem1  9144  wemapwe  9152  rankr1clem  9241  rankr1c  9242  ranklim  9265  r1pwALT  9267  r1pwcl  9268  isfin1-2  9799  isfin1-4  9801  fin71num  9811  axdc3lem2  9865  ltmnq  10386  prlem936  10461  ltsosr  10508  ltasr  10514  xrlenlt  10698  ltxrlt  10703  letri3  10718  ne0gt0  10737  subadd  10881  ltsubadd2  11103  lesubadd2  11105  suble  11110  ltsub23  11112  ltaddpos2  11123  ltsubpos  11124  subge02  11148  ltord2  11161  leord2  11162  ltaddsublt  11259  divmul  11293  divmul3  11295  rec11r  11331  ltdiv1  11496  ltdivmul2  11509  ledivmul2  11511  ltrec  11514  ltdiv2  11518  negfi  11581  negiso  11613  nnle1eq1  11659  avgle1  11869  avgle2  11870  avgle  11871  nn0le0eq0  11917  elz2  11991  znnnlt1  12001  zleltp1  12025  difrp  12420  xrltlen  12532  dfle2  12533  xrletri3  12540  xgepnf  12551  xlemnf  12553  qbtwnre  12585  xltnegi  12602  supxrre  12713  infxrre  12722  elioo5  12787  elfz5  12893  elfzm11  12971  predfz  13025  flbi  13179  flbi2  13180  fldiv4lem1div2uz2  13199  fznnfl  13223  zmodid2  13260  2submod  13293  lt2sq  13491  le2sq  13492  sqlecan  13564  bcval5  13671  pfxsuffeqwrdeq  14053  shftfib  14424  mulre  14473  cnpart  14592  sqrlem6  14600  sqrmo  14604  elicc4abs  14672  abs2difabs  14687  cau4  14709  limsupgre  14831  clim2  14854  ello1mpt2  14872  lo1resb  14914  o1resb  14916  climeq  14917  climmpt2  14923  isercoll  15017  caucvgb  15029  fsumabs  15148  isumshft  15186  geomulcvg  15224  absefib  15543  dvdsval3  15603  dvdsabseq  15655  dvdsflip  15659  dvdsssfz1  15660  mod2eq1n2dvds  15688  ndvdsadd  15753  bitscmp  15779  smupvallem  15824  dvdssq  15903  lcmdvds  15944  ncoprmgcdgt1b  15987  isprm3  16019  isprm5  16043  phiprmpw  16105  prmdiv  16114  pc11  16208  pcz  16209  pockthlem  16233  prmreclem2  16245  prmreclem4  16247  prmreclem6  16249  1arith  16255  vdwapun  16302  rami  16343  ramcl  16357  pwsle  16757  ercpbllem  16813  invsym  17024  funcres2c  17163  latnle  17687  grpinvcnv  18099  subgacs  18245  eqger  18262  gexdvds2  18632  pgpfi1  18642  pgpfi  18652  lsmass  18717  lssnle  18722  lsmdisj3b  18738  lsmhash  18753  ablsubadd  18854  gsumval3lem2  18948  subgdmdprd  19078  pgpfac1lem2  19119  dvdsr02  19328  drngid2  19440  issubrg3  19485  sdrgacs  19502  lssacs  19661  psrbaglefi  20073  coe1mul2lem1  20354  prmirred  20560  chrdvds  20593  chrcong  20594  chrnzr  20595  znleval  20619  znleval2  20620  cygznlem3  20634  frlmbas  20817  elfilspd  20865  lindfmm  20889  islindf4  20900  islindf5  20901  mdetunilem9  21147  isneip  21631  neiptopnei  21658  lpdifsn  21669  restopnb  21701  restopn2  21703  restdis  21704  restperf  21710  lmbr2  21785  cncls2  21799  cnprest  21815  cnprest2  21816  iscnrm2  21864  ist0-2  21870  ist1-3  21875  ishaus2  21877  cmpfi  21934  dfconn2  21945  1stccnp  21988  subislly  22007  hausmapdom  22026  tx1cn  22135  tx2cn  22136  txcnmpt  22150  txrest  22157  hauseqlcld  22172  tgqtop  22238  qtopcld  22239  ordthmeolem  22327  trfil2  22413  trfil3  22414  trnei  22418  ufildr  22457  fmfg  22475  rnelfm  22479  fmfnfm  22484  elflim  22497  flimrest  22509  cnflf  22528  cnflf2  22529  ptcmplem2  22579  ghmcnp  22640  tsmssubm  22668  iscfilu  22814  xmetgt0  22885  prdsxmetlem  22895  blcomps  22920  blcom  22921  xblpnfps  22922  xblpnf  22923  blpnf  22924  xmeter  22960  setsxms  23006  imasf1obl  23015  stdbdbl  23044  metrest  23051  metuel2  23092  dscopn  23100  xrtgioo  23331  metdstri  23376  cnmpopc  23449  iihalf2  23454  icopnfhmeo  23464  evth2  23481  lmmbr3  23780  iscau3  23798  metcld  23826  cfilucfil3  23840  srabn  23880  rrxmet  23928  minveclem4  23952  evthicc2  23978  ovolgelb  23998  shft2rab  24026  ovolshftlem1  24027  sca2rab  24030  ovolscalem1  24031  ioombl1lem4  24079  mbfmulc2lem  24165  ismbf3d  24172  mbfsup  24182  mbfinf  24183  i1f1lem  24207  i1fmulclem  24220  mbfi1fseqlem4  24236  itg2seq  24260  ditgneg  24372  limcdif  24391  limcnlp  24393  cnplimc  24402  rolle  24504  mvth  24506  dvne0  24525  lhop1lem  24527  itgsubst  24563  mdegle0  24588  deg1leb  24606  deg1le0  24622  q1peqb  24665  coemulhi  24761  dgrlt  24773  plydivlem3  24801  vieta1lem2  24817  aannenlem1  24834  ulmres  24893  reefiso  24953  pilem3  24958  ellogdm  25137  root1eq1  25251  angpieqvdlem  25321  angpieqvdlem2  25322  quad2  25332  1cubr  25335  quart  25354  rlimcnp  25459  wilthlem2  25562  isppw  25607  dvdsflsumcom  25681  fsumvma  25705  logfac2  25709  chpchtsum  25711  dchrmulcl  25741  dchrresb  25751  bclbnd  25772  bposlem1  25776  bposlem5  25780  gausslemma2dlem0c  25850  lgsquadlem1  25872  m1lgs  25880  2lgsoddprmlem2  25901  dchrisumlem3  25983  dchrisum0lem1  26008  tgjustr  26176  trgcgrg  26217  lnrot1  26325  islnopp  26441  ismidb  26480  islmib  26489  axsegconlem6  26624  axeuclidlem  26664  axcontlem2  26667  axcontlem4  26669  axcontlem12  26677  ausgrusgrb  26866  nb3grpr2  27081  cplgr2v  27130  umgr2v2enb1  27224  crctcsh  27518  clwwlknonwwlknonb  27801  eupth2lems  27933  nmoreltpnf  28462  isblo2  28476  nmlnogt0  28490  phoeqi  28550  ubthlem2  28564  hire  28787  normgt0  28820  ho01i  29521  ho02i  29522  hoeq1  29523  hoeq2  29524  nmopreltpnf  29562  adjeq  29628  leop  29816  leopmul2i  29828  pjnormssi  29861  pjimai  29869  jplem1  29961  mddmd2  30002  mdslmd1lem1  30018  mdslmd1lem2  30019  superpos  30047  atnssm0  30069  dmdbr5ati  30115  disjunsn  30261  fcoinvbr  30275  ofpreima  30327  funcnv5mpt  30330  isoun  30352  fpwrelmapffslem  30383  fpwrelmap  30384  iocinioc2  30417  xrdifh  30418  nndiffz1  30424  xdivmul  30517  cntzsnid  30612  isarchi2  30730  finexttrb  30940  smatrcl  30949  sqsscirc2  31040  xrmulc1cn  31061  esumfsup  31217  1stmbfm  31406  2ndmbfm  31407  mbfmcnt  31414  eulerpartlems  31506  eulerpartlemd  31512  ballotlemfc0  31638  ballotlemfcc  31639  ballotlemsima  31661  ballotlemfrcn0  31675  sgn3da  31687  reprinfz1  31781  reprdifc  31786  bnj1173  32160  zltp1ne  32234  lfuhgr2  32251  erdszelem7  32330  erdszelem9  32332  iscvm  32392  cvmlift3lem4  32455  sltval2  33049  noextenddif  33061  sleloe  33119  sletri3  33120  fscgr  33427  seglelin  33463  btwnoutside  33472  lineunray  33494  cldbnd  33560  isfne4  33574  fneval  33586  filnetlem4  33615  nndivsub  33691  dfgcd3  34476  fvineqsneu  34563  wl-sbhbt  34659  wl-sbcom2d  34666  wl-sbalnae  34667  wl-ax11-lem8  34693  wl-dfrmof  34724  sin2h  34751  cos2h  34752  matunitlindflem1  34757  matunitlindflem2  34758  matunitlindf  34759  ptrest  34760  poimirlem3  34764  poimirlem4  34765  poimirlem22  34783  poimirlem27  34788  mblfinlem3  34800  mblfinlem4  34801  ismblfin  34802  itg2addnclem  34812  itg2addnclem2  34813  itg2gt0cn  34816  iblabsnclem  34824  ftc1anclem6  34841  areacirclem2  34852  areacirclem5  34855  areacirc  34856  mettrifi  34902  drngoi  35099  eldm4  35401  exanres2  35424  brcoss2  35546  br1cossres2  35554  eldmcoss2  35568  eldm1cossres2  35570  brcosscnv2  35582  erim2  35780  prter3  35887  islshpat  36022  lsatnle  36049  ellkr2  36096  lshpkr  36122  lkr0f2  36166  lduallkr3  36167  lkreqN  36175  cvrval2  36279  isat3  36312  glbconN  36382  hlrelat5N  36406  cvrval4N  36419  atlt  36442  1cvrco  36477  pmaple  36766  isline2  36779  isline4N  36782  elpaddn0  36805  elpadd2at2  36812  cdlemkid4  37939  dia0  38057  cdlemm10N  38123  dibglbN  38171  dihmeetlem4preN  38311  dochkrshp3  38393  dvh4dimlem  38448  lcfl5  38501  mapdpglem3  38680  mapdheq  38733  hdmap1eq  38806  hdmapval2lem  38836  hdmapoc  38936  hlhillcs  38963  renegadd  39069  resubadd  39076  fz1eqin  39233  diophin  39236  jm2.19  39457  rmxdiophlem  39479  pw2f1ocnv  39501  wepwsolem  39509  gicabl  39566  idomodle  39663  isdomn3  39671  ntrclsfveq2  40278  ntrclsss  40280  ntrclsk4  40289  extoimad  40382  radcnvrat  40513  bcc0  40539  supxrre3rnmpt  41570  clim2f  41784  clim2f2  41818  liminfreuzlem  41950  liminfltlem  41952  xlimmnflimsup2  42000  xlimpnfliminf2  42009  xlimlimsupleliminf  42011  opprb  43134  funbrafv2b  43226  dfafn5a  43227  leaddsuble  43365  iccpartgtprec  43414  flsqrt  43590  dfeven2  43648  dfodd3  43649  lindslinindimp2lem4  44350  snlindsntor  44360  regt1loggt0  44430  elbigo2  44446  elbigolo1  44451  fldivexpfllog2  44459  nnlog2ge0lt1  44460  blenpw2m1  44473
  Copyright terms: Public domain W3C validator