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  706  sb3b  2476  sbcom3  2506  sbal1  2528  sbal2  2529  2reu4lem  4526  issn  4834  disjprgw  5144  disjprg  5145  reuhypd  5418  snelpwg  5443  ordtri3  6401  ordsssuc  6454  iota1  6521  funbrfv2b  6950  dffn5  6951  feqmptdf  6963  unima  6967  dmfco  6988  fneqeql  7048  f1ompt  7111  dff13  7254  fliftcnv  7308  soisores  7324  isotr  7333  isoini  7335  caovord3  7620  releldm2  8029  fimaproj  8121  brtpos  8220  tpostpos  8231  oe1m  8545  oawordri  8550  oalimcl  8560  omlimcl  8578  omabs  8650  iserd  8729  qliftel  8794  qliftfun  8796  qliftf  8799  ecopovsym  8813  pw2f1olem  9076  mapen  9141  findcard3  9285  suppeqfsuppbi  9377  mapfien  9403  supisolem  9468  cantnflem1  9684  wemapwe  9692  rankr1clem  9815  rankr1c  9816  ranklim  9839  r1pwALT  9841  r1pwcl  9842  isfin1-2  10380  isfin1-4  10382  fin71num  10392  axdc3lem2  10446  ltmnq  10967  prlem936  11042  ltsosr  11089  ltasr  11095  xrlenlt  11279  ltxrlt  11284  letri3  11299  ne0gt0  11319  subadd  11463  ltsubadd2  11685  lesubadd2  11687  suble  11692  ltsub23  11694  ltaddpos2  11705  ltsubpos  11706  subge02  11730  ltord2  11743  leord2  11744  ltaddsublt  11841  divmul  11875  divmul3  11877  rec11r  11913  ltdiv1  12078  ltdivmul2  12091  ledivmul2  12093  ltrec  12096  ltdiv2  12100  negfi  12163  negiso  12194  nnle1eq1  12242  avgle1  12452  avgle2  12453  avgle  12454  nn0le0eq0  12500  elz2  12576  znnnlt1  12589  zleltp1  12613  difrp  13012  xrltlen  13125  dfle2  13126  xrletri3  13133  xgepnf  13144  xlemnf  13146  qbtwnre  13178  xltnegi  13195  supxrre  13306  infxrre  13315  elioo5  13381  elfz5  13493  elfzm11  13572  predfz  13626  flbi  13781  flbi2  13782  fldiv4lem1div2uz2  13801  fznnfl  13827  zmodid2  13864  2submod  13897  lt2sq  14098  le2sq  14099  sqlecan  14173  bcval5  14278  pfxsuffeqwrdeq  14648  shftfib  15019  mulre  15068  cnpart  15187  01sqrexlem6  15194  sqrmo  15198  elicc4abs  15266  abs2difabs  15281  cau4  15303  limsupgre  15425  clim2  15448  ello1mpt2  15466  lo1resb  15508  o1resb  15510  climeq  15511  climmpt2  15517  isercoll  15614  caucvgb  15626  fsumabs  15747  isumshft  15785  geomulcvg  15822  absefib  16141  dvdsval3  16201  dvdsabseq  16256  dvdsflip  16260  dvdsssfz1  16261  mod2eq1n2dvds  16290  ndvdsadd  16353  bitscmp  16379  smupvallem  16424  dvdssq  16504  lcmdvds  16545  ncoprmgcdgt1b  16588  isprm3  16620  isprm5  16644  phiprmpw  16709  prmdiv  16718  pc11  16813  pcz  16814  pockthlem  16838  prmreclem2  16850  prmreclem4  16852  prmreclem6  16854  1arith  16860  vdwapun  16907  rami  16948  ramcl  16962  pwsle  17438  ercpbllem  17494  invsym  17709  funcres2c  17852  latnle  18426  grpinvcnv  18891  subgacs  19041  eqger  19058  gexdvds2  19453  pgpfi1  19463  pgpfi  19473  lsmass  19537  lssnle  19542  lsmdisj3b  19558  lsmhash  19573  ablsubadd  19677  gsumval3lem2  19774  subgdmdprd  19904  pgpfac1lem2  19945  dvdsr02  20186  issubrg3  20347  drngid2  20378  sdrgunit  20412  sdrgacs  20417  lssacs  20578  prmirred  21044  chrdvds  21080  chrcong  21081  chrnzr  21082  znleval  21110  znleval2  21111  cygznlem3  21125  frlmbas  21310  elfilspd  21358  lindfmm  21382  islindf4  21393  islindf5  21394  psrbaglefi  21485  psrbaglefiOLD  21486  coe1mul2lem1  21789  mdetunilem9  22122  isneip  22609  neiptopnei  22636  lpdifsn  22647  restopnb  22679  restopn2  22681  restdis  22682  restperf  22688  lmbr2  22763  cncls2  22777  cnprest  22793  cnprest2  22794  iscnrm2  22842  ist0-2  22848  ist1-3  22853  ishaus2  22855  cmpfi  22912  dfconn2  22923  1stccnp  22966  subislly  22985  hausmapdom  23004  tx1cn  23113  tx2cn  23114  txcnmpt  23128  txrest  23135  hauseqlcld  23150  tgqtop  23216  qtopcld  23217  ordthmeolem  23305  trfil2  23391  trfil3  23392  trnei  23396  ufildr  23435  fmfg  23453  rnelfm  23457  fmfnfm  23462  elflim  23475  flimrest  23487  cnflf  23506  cnflf2  23507  ptcmplem2  23557  ghmcnp  23619  tsmssubm  23647  iscfilu  23793  xmetgt0  23864  prdsxmetlem  23874  blcomps  23899  blcom  23900  xblpnfps  23901  xblpnf  23902  blpnf  23903  xmeter  23939  setsxms  23987  imasf1obl  23997  stdbdbl  24026  metrest  24033  metuel2  24074  dscopn  24082  xrtgioo  24322  metdstri  24367  cnmpopc  24444  iihalf2  24449  icopnfhmeo  24459  evth2  24476  lmmbr3  24777  iscau3  24795  metcld  24823  cfilucfil3  24837  srabn  24877  rrxmet  24925  minveclem4  24949  evthicc2  24977  ovolgelb  24997  shft2rab  25025  ovolshftlem1  25026  sca2rab  25029  ovolscalem1  25030  ioombl1lem4  25078  mbfmulc2lem  25164  ismbf3d  25171  mbfsup  25181  mbfinf  25182  i1f1lem  25206  i1fmulclem  25220  mbfi1fseqlem4  25236  itg2seq  25260  ditgneg  25374  limcdif  25393  limcnlp  25395  cnplimc  25404  rolle  25507  mvth  25509  dvne0  25528  lhop1lem  25530  itgsubst  25566  mdegle0  25595  deg1leb  25613  deg1le0  25629  q1peqb  25672  coemulhi  25768  dgrlt  25780  plydivlem3  25808  vieta1lem2  25824  aannenlem1  25841  ulmres  25900  reefiso  25960  pilem3  25965  ellogdm  26147  root1eq1  26263  angpieqvdlem  26333  angpieqvdlem2  26334  quad2  26344  1cubr  26347  quart  26366  rlimcnp  26470  wilthlem2  26573  isppw  26618  dvdsflsumcom  26692  fsumvma  26716  logfac2  26720  chpchtsum  26722  dchrmulcl  26752  dchrresb  26762  bclbnd  26783  bposlem1  26787  bposlem5  26791  gausslemma2dlem0c  26861  lgsquadlem1  26883  m1lgs  26891  2lgsoddprmlem2  26912  dchrisumlem3  26994  dchrisum0lem1  27019  sltval2  27159  noextenddif  27171  sleloe  27257  sletri3  27258  eqscut  27307  elmade2  27364  sltadd1  27478  negsunif  27532  sltsub1  27546  sltsubadd2d  27560  mulsproplem12  27586  sltmul2  27626  sltmul1d  27628  divsmulw  27643  sltdivmul2wd  27650  tgjustr  27756  trgcgrg  27797  lnrot1  27905  islnopp  28021  ismidb  28060  islmib  28069  axsegconlem6  28211  axeuclidlem  28251  axcontlem2  28254  axcontlem4  28256  axcontlem12  28264  ausgrusgrb  28456  nb3grpr2  28671  cplgr2v  28720  umgr2v2enb1  28814  crctcsh  29109  clwwlknonwwlknonb  29390  eupth2lems  29522  nmoreltpnf  30053  isblo2  30067  nmlnogt0  30081  phoeqi  30141  ubthlem2  30155  hire  30378  normgt0  30411  ho01i  31112  ho02i  31113  hoeq1  31114  hoeq2  31115  nmopreltpnf  31153  adjeq  31219  leop  31407  leopmul2i  31419  pjnormssi  31452  pjimai  31460  jplem1  31552  mddmd2  31593  mdslmd1lem1  31609  mdslmd1lem2  31610  superpos  31638  atnssm0  31660  dmdbr5ati  31706  disjunsn  31856  fcoinvbr  31867  ofpreima  31921  funcnv5mpt  31924  suppiniseg  31939  isoun  31954  fpwrelmapffslem  31988  fpwrelmap  31989  iocinioc2  32021  xrdifh  32022  nndiffz1  32028  xdivmul  32122  cntzsnid  32244  isarchi2  32362  elrsp  32517  lsmsnpridl  32539  lsmssass  32543  ghmqusker  32563  finexttrb  32772  smatrcl  32807  rhmpreimacnlem  32895  sqsscirc2  32920  xrmulc1cn  32941  esumfsup  33099  1stmbfm  33290  2ndmbfm  33291  mbfmcnt  33298  eulerpartlems  33390  eulerpartlemd  33396  ballotlemfc0  33522  ballotlemfcc  33523  ballotlemsima  33545  ballotlemfrcn0  33559  sgn3da  33571  reprinfz1  33665  reprdifc  33670  bnj1173  34044  zltp1ne  34130  lfuhgr2  34140  erdszelem7  34219  erdszelem9  34221  iscvm  34281  cvmlift3lem4  34344  fscgr  35083  seglelin  35119  btwnoutside  35128  lineunray  35150  cldbnd  35259  isfne4  35273  fneval  35285  filnetlem4  35314  nndivsub  35390  bj-gabima  35868  dfgcd3  36253  fvineqsneu  36340  wl-sbhbt  36467  wl-sbcom2d  36474  wl-sbalnae  36475  wl-ax11-lem8  36502  sin2h  36526  cos2h  36527  matunitlindflem1  36532  matunitlindflem2  36533  matunitlindf  36534  ptrest  36535  poimirlem3  36539  poimirlem4  36540  poimirlem22  36558  poimirlem27  36563  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  itg2addnclem  36587  itg2addnclem2  36588  itg2gt0cn  36591  iblabsnclem  36599  ftc1anclem6  36614  areacirclem2  36625  areacirclem5  36628  areacirc  36629  mettrifi  36673  drngoi  36867  eldm4  37190  exanres2  37214  disjecxrn  37307  brcoss2  37350  br1cossres2  37358  eldmcoss2  37377  eldm1cossres2  37379  brcosscnv2  37391  erimeq2  37596  disjlem19  37719  prter3  37800  islshpat  37935  lsatnle  37962  ellkr2  38009  lshpkr  38035  lkr0f2  38079  lduallkr3  38080  lkreqN  38088  cvrval2  38192  isat3  38225  glbconN  38295  glbconNOLD  38296  hlrelat5N  38320  cvrval4N  38333  atlt  38356  1cvrco  38391  pmaple  38680  isline2  38693  isline4N  38696  elpaddn0  38719  elpadd2at2  38726  cdlemkid4  39853  dia0  39971  cdlemm10N  40037  dibglbN  40085  dihmeetlem4preN  40225  dochkrshp3  40307  dvh4dimlem  40362  lcfl5  40415  mapdpglem3  40594  mapdheq  40647  hdmap1eq  40720  hdmapval2lem  40750  hdmapoc  40850  hlhillcs  40881  lcmineqlem18  40959  fsuppssind  41213  dvdsexpb  41281  renegadd  41293  resubadd  41300  mulgt0b2d  41381  fz1eqin  41555  diophin  41558  jm2.19  41780  rmxdiophlem  41802  pw2f1ocnv  41824  wepwsolem  41832  gicabl  41889  idomodle  41986  isdomn3  41994  onsupmaxb  42036  cantnf2  42123  tfsconcatb0  42142  tfsnfin  42150  ntrclsfveq2  42860  ntrclsss  42862  ntrclsk4  42871  extoimad  42964  radcnvrat  43121  bcc0  43147  supxrre3rnmpt  44187  clim2f  44400  clim2f2  44434  liminfreuzlem  44566  liminfltlem  44568  xlimmnflimsup2  44616  xlimpnfliminf2  44625  xlimlimsupleliminf  44627  opprb  45789  funbrafv2b  45915  dfafn5a  45916  leaddsuble  46053  iccpartgtprec  46136  flsqrt  46309  dfeven2  46365  dfodd3  46366  lindslinindimp2lem4  47190  snlindsntor  47200  regt1loggt0  47270  elbigo2  47286  elbigolo1  47291  fldivexpfllog2  47299  nnlog2ge0lt1  47300  blenpw2m1  47313  naryfvalelwrdf  47367  isprsd  47636  functhinclem1  47709  thincciso  47717  thinciso  47728  prstcprs  47743  postc  47750