Theorem bitr4d 282

Description: Deduction form of bitr4i 278. (Contributed by NM, 30-Jun-1993.)

Hypotheses

Ref	Expression
bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
bitr4d	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	bicomd 222	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitr2d  307  3bitr2rd  308  3bitr4d  311  3bitr4rd  312  bianabs  543  mpbirand  705  sb3b  2475  sbcom3  2508  sbal1  2531  sbal2  2532  2reu4lem  4462  issn  4769  disjprgw  5076  disjprg  5077  reuhypd  5351  ordtri3  6317  ordsssuc  6369  iota1  6435  funbrfv2b  6859  dffn5  6860  feqmptdf  6871  unima  6875  dmfco  6896  fneqeql  6955  f1ompt  7017  dff13  7160  fliftcnv  7214  soisores  7230  isotr  7239  isoini  7241  caovord3  7517  releldm2  7916  fimaproj  8007  brtpos  8082  tpostpos  8093  oe1m  8407  oawordri  8412  oalimcl  8422  omlimcl  8440  omabs  8512  iserd  8555  qliftel  8620  qliftfun  8622  qliftf  8625  ecopovsym  8639  pw2f1olem  8901  mapen  8966  suppeqfsuppbi  9186  mapfien  9211  supisolem  9276  cantnflem1  9491  wemapwe  9499  rankr1clem  9622  rankr1c  9623  ranklim  9646  r1pwALT  9648  r1pwcl  9649  isfin1-2  10187  isfin1-4  10189  fin71num  10199  axdc3lem2  10253  ltmnq  10774  prlem936  10849  ltsosr  10896  ltasr  10902  xrlenlt  11086  ltxrlt  11091  letri3  11106  ne0gt0  11126  subadd  11270  ltsubadd2  11492  lesubadd2  11494  suble  11499  ltsub23  11501  ltaddpos2  11512  ltsubpos  11513  subge02  11537  ltord2  11550  leord2  11551  ltaddsublt  11648  divmul  11682  divmul3  11684  rec11r  11720  ltdiv1  11885  ltdivmul2  11898  ledivmul2  11900  ltrec  11903  ltdiv2  11907  negfi  11970  negiso  12001  nnle1eq1  12049  avgle1  12259  avgle2  12260  avgle  12261  nn0le0eq0  12307  elz2  12383  znnnlt1  12393  zleltp1  12417  difrp  12814  xrltlen  12926  dfle2  12927  xrletri3  12934  xgepnf  12945  xlemnf  12947  qbtwnre  12979  xltnegi  12996  supxrre  13107  infxrre  13116  elioo5  13182  elfz5  13294  elfzm11  13373  predfz  13427  flbi  13582  flbi2  13583  fldiv4lem1div2uz2  13602  fznnfl  13628  zmodid2  13665  2submod  13698  lt2sq  13898  le2sq  13899  sqlecan  13971  bcval5  14078  pfxsuffeqwrdeq  14456  shftfib  14828  mulre  14877  cnpart  14996  sqrlem6  15004  sqrmo  15008  elicc4abs  15076  abs2difabs  15091  cau4  15113  limsupgre  15235  clim2  15258  ello1mpt2  15276  lo1resb  15318  o1resb  15320  climeq  15321  climmpt2  15327  isercoll  15424  caucvgb  15436  fsumabs  15558  isumshft  15596  geomulcvg  15633  absefib  15952  dvdsval3  16012  dvdsabseq  16067  dvdsflip  16071  dvdsssfz1  16072  mod2eq1n2dvds  16101  ndvdsadd  16164  bitscmp  16190  smupvallem  16235  dvdssq  16317  lcmdvds  16358  ncoprmgcdgt1b  16401  isprm3  16433  isprm5  16457  phiprmpw  16522  prmdiv  16531  pc11  16626  pcz  16627  pockthlem  16651  prmreclem2  16663  prmreclem4  16665  prmreclem6  16667  1arith  16673  vdwapun  16720  rami  16761  ramcl  16775  pwsle  17248  ercpbllem  17304  invsym  17519  funcres2c  17662  latnle  18236  grpinvcnv  18688  subgacs  18834  eqger  18851  gexdvds2  19235  pgpfi1  19245  pgpfi  19255  lsmass  19320  lssnle  19325  lsmdisj3b  19341  lsmhash  19356  ablsubadd  19458  gsumval3lem2  19552  subgdmdprd  19682  pgpfac1lem2  19723  dvdsr02  19943  drngid2  20052  issubrg3  20097  sdrgacs  20114  lssacs  20274  prmirred  20741  chrdvds  20777  chrcong  20778  chrnzr  20779  znleval  20807  znleval2  20808  cygznlem3  20822  frlmbas  21007  elfilspd  21055  lindfmm  21079  islindf4  21090  islindf5  21091  psrbaglefi  21180  psrbaglefiOLD  21181  coe1mul2lem1  21483  mdetunilem9  21814  isneip  22301  neiptopnei  22328  lpdifsn  22339  restopnb  22371  restopn2  22373  restdis  22374  restperf  22380  lmbr2  22455  cncls2  22469  cnprest  22485  cnprest2  22486  iscnrm2  22534  ist0-2  22540  ist1-3  22545  ishaus2  22547  cmpfi  22604  dfconn2  22615  1stccnp  22658  subislly  22677  hausmapdom  22696  tx1cn  22805  tx2cn  22806  txcnmpt  22820  txrest  22827  hauseqlcld  22842  tgqtop  22908  qtopcld  22909  ordthmeolem  22997  trfil2  23083  trfil3  23084  trnei  23088  ufildr  23127  fmfg  23145  rnelfm  23149  fmfnfm  23154  elflim  23167  flimrest  23179  cnflf  23198  cnflf2  23199  ptcmplem2  23249  ghmcnp  23311  tsmssubm  23339  iscfilu  23485  xmetgt0  23556  prdsxmetlem  23566  blcomps  23591  blcom  23592  xblpnfps  23593  xblpnf  23594  blpnf  23595  xmeter  23631  setsxms  23679  imasf1obl  23689  stdbdbl  23718  metrest  23725  metuel2  23766  dscopn  23774  xrtgioo  24014  metdstri  24059  cnmpopc  24136  iihalf2  24141  icopnfhmeo  24151  evth2  24168  lmmbr3  24469  iscau3  24487  metcld  24515  cfilucfil3  24529  srabn  24569  rrxmet  24617  minveclem4  24641  evthicc2  24669  ovolgelb  24689  shft2rab  24717  ovolshftlem1  24718  sca2rab  24721  ovolscalem1  24722  ioombl1lem4  24770  mbfmulc2lem  24856  ismbf3d  24863  mbfsup  24873  mbfinf  24874  i1f1lem  24898  i1fmulclem  24912  mbfi1fseqlem4  24928  itg2seq  24952  ditgneg  25066  limcdif  25085  limcnlp  25087  cnplimc  25096  rolle  25199  mvth  25201  dvne0  25220  lhop1lem  25222  itgsubst  25258  mdegle0  25287  deg1leb  25305  deg1le0  25321  q1peqb  25364  coemulhi  25460  dgrlt  25472  plydivlem3  25500  vieta1lem2  25516  aannenlem1  25533  ulmres  25592  reefiso  25652  pilem3  25657  ellogdm  25839  root1eq1  25953  angpieqvdlem  26023  angpieqvdlem2  26024  quad2  26034  1cubr  26037  quart  26056  rlimcnp  26160  wilthlem2  26263  isppw  26308  dvdsflsumcom  26382  fsumvma  26406  logfac2  26410  chpchtsum  26412  dchrmulcl  26442  dchrresb  26452  bclbnd  26473  bposlem1  26477  bposlem5  26481  gausslemma2dlem0c  26551  lgsquadlem1  26573  m1lgs  26581  2lgsoddprmlem2  26602  dchrisumlem3  26684  dchrisum0lem1  26709  tgjustr  26880  trgcgrg  26921  lnrot1  27029  islnopp  27145  ismidb  27184  islmib  27193  axsegconlem6  27335  axeuclidlem  27375  axcontlem2  27378  axcontlem4  27380  axcontlem12  27388  ausgrusgrb  27580  nb3grpr2  27795  cplgr2v  27844  umgr2v2enb1  27938  crctcsh  28234  clwwlknonwwlknonb  28515  eupth2lems  28647  nmoreltpnf  29176  isblo2  29190  nmlnogt0  29204  phoeqi  29264  ubthlem2  29278  hire  29501  normgt0  29534  ho01i  30235  ho02i  30236  hoeq1  30237  hoeq2  30238  nmopreltpnf  30276  adjeq  30342  leop  30530  leopmul2i  30542  pjnormssi  30575  pjimai  30583  jplem1  30675  mddmd2  30716  mdslmd1lem1  30732  mdslmd1lem2  30733  superpos  30761  atnssm0  30783  dmdbr5ati  30829  disjunsn  30978  fcoinvbr  30992  ofpreima  31047  funcnv5mpt  31050  suppiniseg  31065  isoun  31079  fpwrelmapffslem  31112  fpwrelmap  31113  iocinioc2  31145  xrdifh  31146  nndiffz1  31152  xdivmul  31244  cntzsnid  31366  isarchi2  31484  elrsp  31614  lsmsnpridl  31631  lsmssass  31635  finexttrb  31782  smatrcl  31791  rhmpreimacnlem  31879  sqsscirc2  31904  xrmulc1cn  31925  esumfsup  32083  1stmbfm  32272  2ndmbfm  32273  mbfmcnt  32280  eulerpartlems  32372  eulerpartlemd  32378  ballotlemfc0  32504  ballotlemfcc  32505  ballotlemsima  32527  ballotlemfrcn0  32541  sgn3da  32553  reprinfz1  32647  reprdifc  32652  bnj1173  33027  zltp1ne  33113  lfuhgr2  33125  erdszelem7  33204  erdszelem9  33206  iscvm  33266  cvmlift3lem4  33329  sltval2  33904  noextenddif  33916  sleloe  34002  sletri3  34003  eqscut  34044  elmade2  34097  fscgr  34427  seglelin  34463  btwnoutside  34472  lineunray  34494  cldbnd  34560  isfne4  34574  fneval  34586  filnetlem4  34615  nndivsub  34691  bj-gabima  35172  dfgcd3  35539  fvineqsneu  35626  wl-sbhbt  35753  wl-sbcom2d  35760  wl-sbalnae  35761  wl-ax11-lem8  35787  sin2h  35811  cos2h  35812  matunitlindflem1  35817  matunitlindflem2  35818  matunitlindf  35819  ptrest  35820  poimirlem3  35824  poimirlem4  35825  poimirlem22  35843  poimirlem27  35848  mblfinlem3  35860  mblfinlem4  35861  ismblfin  35862  itg2addnclem  35872  itg2addnclem2  35873  itg2gt0cn  35876  iblabsnclem  35884  ftc1anclem6  35899  areacirclem2  35910  areacirclem5  35913  areacirc  35914  mettrifi  35959  drngoi  36153  eldm4  36452  exanres2  36475  brcoss2  36597  br1cossres2  36605  eldmcoss2  36619  eldm1cossres2  36621  brcosscnv2  36633  erim2  36831  prter3  36938  islshpat  37073  lsatnle  37100  ellkr2  37147  lshpkr  37173  lkr0f2  37217  lduallkr3  37218  lkreqN  37226  cvrval2  37330  isat3  37363  glbconN  37433  hlrelat5N  37457  cvrval4N  37470  atlt  37493  1cvrco  37528  pmaple  37817  isline2  37830  isline4N  37833  elpaddn0  37856  elpadd2at2  37863  cdlemkid4  38990  dia0  39108  cdlemm10N  39174  dibglbN  39222  dihmeetlem4preN  39362  dochkrshp3  39444  dvh4dimlem  39499  lcfl5  39552  mapdpglem3  39731  mapdheq  39784  hdmap1eq  39857  hdmapval2lem  39887  hdmapoc  39987  hlhillcs  40018  lcmineqlem18  40096  fsuppssind  40319  dvdsexpb  40379  renegadd  40392  resubadd  40399  mulgt0b2d  40467  fz1eqin  40628  diophin  40631  jm2.19  40853  rmxdiophlem  40875  pw2f1ocnv  40897  wepwsolem  40905  gicabl  40962  idomodle  41059  isdomn3  41067  ntrclsfveq2  41709  ntrclsss  41711  ntrclsk4  41720  extoimad  41813  radcnvrat  41970  bcc0  41996  supxrre3rnmpt  43017  clim2f  43226  clim2f2  43260  liminfreuzlem  43392  liminfltlem  43394  xlimmnflimsup2  43442  xlimpnfliminf2  43451  xlimlimsupleliminf  43453  opprb  44583  funbrafv2b  44709  dfafn5a  44710  leaddsuble  44847  iccpartgtprec  44930  flsqrt  45103  dfeven2  45159  dfodd3  45160  lindslinindimp2lem4  45860  snlindsntor  45870  regt1loggt0  45940  elbigo2  45956  elbigolo1  45961  fldivexpfllog2  45969  nnlog2ge0lt1  45970  blenpw2m1  45983  naryfvalelwrdf  46037  isprsd  46307  functhinclem1  46380  thincciso  46388  thinciso  46399  prstcprs  46414  postc  46421