Theorem bitr4d 285

Description: Deduction form of bitr4i 281. (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 226	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr2d  310  3bitr2rd  311  3bitr4d  314  3bitr4rd  315  bianabs  550  mpbirand  719  sb3b  2507  sbcom3  2537  sbal1  2559  sbal2  2560  2reu4lem  4483  issn  4796  disjprg  5104  reuhypd  5389  snelpwg  5423  ordtri3  6397  ordsssuc  6452  iota1  6515  funbrfv2b  6938  dffn5  6939  feqmptdf  6951  unima  6956  dmfco  6977  fneqeql  7041  f1ompt  7106  dff13  7252  fliftcnv  7309  soisores  7325  isotr  7334  isoini  7336  caovord3  7625  releldm2  8038  fimaproj  8129  brtpos  8229  tpostpos  8240  oe1m  8528  oawordri  8533  oalimcl  8543  omlimcl  8561  omabs  8635  iserd  8719  qliftel  8796  qliftfun  8798  qliftf  8801  ecopovsym  8815  pw2f1olem  9067  mapen  9127  findcard3  9241  tfsnfin2  9318  suppeqfsuppbi  9337  mapfien  9366  supisolem  9432  cantnflem1  9656  wemapwe  9664  rankr1clem  9790  rankr1c  9791  ranklim  9814  r1pwALT  9816  r1pwcl  9817  isfin1-2  10375  isfin1-4  10377  fin71num  10387  axdc3lem2  10441  infinfg  10556  ltmnq  10963  prlem936  11038  ltsosr  11085  ltasr  11091  xrlenlt  11280  ltxrlt  11286  letri3  11301  ne0gt0  11321  subadd  11466  ltsubadd2  11691  lesubadd2  11693  suble  11698  ltsub23  11700  ltaddpos2  11711  ltsubpos  11712  subge02  11736  ltord2  11749  leord2  11750  ltaddsublt  11847  divmul  11881  divmul3  11883  rec11r  11920  ltdiv1  12085  ltdivmul2  12098  ledivmul2  12100  ltrec  12103  ltdiv2  12107  negfi  12170  negiso  12201  nnle1eq1  12272  avgle1  12490  avgle2  12491  avgle  12492  nn0le0eq0  12538  elz2  12615  znnnlt1  12627  zleltp1  12651  difrp  13062  xrltlen  13177  dfle2  13178  xrletri3  13185  xgepnf  13197  xlemnf  13199  qbtwnre  13231  xltnegi  13248  supxrre  13359  infxrre  13369  elioo5  13436  elfz5  13550  elfzm11  13630  predfz  13688  flbi  13856  flbi2  13857  fldiv4lem1div2uz2  13876  fznnfl  13902  zmodid2  13939  2submod  13975  lt2sq  14176  le2sq  14177  sqlecan  14252  bcval5  14361  pfxsuffeqwrdeq  14742  shftfib  15116  sgn3da  15145  mulre  15179  cnpart  15298  01sqrexlem6  15305  sqrmo  15309  elicc4abs  15378  abs2difabs  15393  cau4  15415  limsupgre  15539  clim2  15562  ello1mpt2  15580  lo1resb  15622  o1resb  15624  climeq  15625  climmpt2  15631  isercoll  15726  caucvgb  15738  fsumabs  15860  isumshft  15900  geomulcvg  15937  absefib  16260  dvdsval3  16320  addmulmodb  16329  dvdsabseq  16377  dvdsflip  16381  dvdsssfz1  16382  mod2eq1n2dvds  16411  ndvdsadd  16474  bitscmp  16502  smupvallem  16547  dvdssq  16631  lcmdvds  16672  ncoprmgcdgt1b  16715  isprm3  16747  isprm5  16772  phiprmpw  16841  prmdiv  16850  pc11  16946  pcz  16947  pockthlem  16971  prmreclem2  16983  prmreclem4  16985  prmreclem6  16987  1arith  16993  vdwapun  17040  rami  17081  ramcl  17095  pwsle  17552  ercpbllem  17608  invsym  17825  funcres2c  17966  latnle  18535  grpinvcnv  19079  subgacs  19233  eqger  19252  ghmqusker  19363  gexdvds2  19661  pgpfi1  19671  pgpfi  19681  lsmass  19745  lssnle  19750  lsmdisj3b  19766  lsmhash  19781  ablsubadd  19885  gsumval3lem2  19982  subgdmdprd  20112  pgpfac1lem2  20153  dvdsr02  20461  issubrg3  20710  isdomn3  20824  drngid2  20867  sdrgunit  20910  sdrgacs  20915  lssacs  21099  prmirred  21635  chrdvds  21687  chrcong  21688  chrnzr  21691  znleval  21715  znleval2  21716  cygznlem3  21730  frlmbas  21916  elfilspd  21964  lindfmm  21988  islindf4  21999  islindf5  22000  psrbaglefi  22087  coe1mul2lem1  22439  mdetunilem9  22788  isneip  23273  neiptopnei  23300  lpdifsn  23311  restopnb  23343  restopn2  23345  restdis  23346  restperf  23352  lmbr2  23427  cncls2  23441  cnprest  23457  cnprest2  23458  iscnrm2  23506  ist0-2  23512  ist1-3  23517  ishaus2  23519  cmpfi  23576  dfconn2  23587  1stccnp  23630  subislly  23649  hausmapdom  23668  tx1cn  23777  tx2cn  23778  txcnmpt  23792  txrest  23799  hauseqlcld  23814  tgqtop  23880  qtopcld  23881  ordthmeolem  23969  trfil2  24055  trfil3  24056  trnei  24060  ufildr  24099  fmfg  24117  rnelfm  24121  fmfnfm  24126  elflim  24139  flimrest  24151  cnflf  24170  cnflf2  24171  ptcmplem2  24221  ghmcnp  24283  tsmssubm  24311  iscfilu  24455  xmetgt0  24526  prdsxmetlem  24536  blcomps  24561  blcom  24562  xblpnfps  24563  xblpnf  24564  blpnf  24565  xmeter  24601  setsxms  24647  imasf1obl  24656  stdbdbl  24685  metrest  24692  metuel2  24733  dscopn  24741  xrtgioo  24975  metdstri  25020  cnmpopc  25098  iihalf2  25103  icopnfhmeo  25113  evth2  25130  lmmbr3  25430  iscau3  25448  metcld  25476  cfilucfil3  25490  srabn  25530  rrxmet  25578  minveclem4  25602  evthicc2  25630  ovolgelb  25650  shft2rab  25678  ovolshftlem1  25679  sca2rab  25682  ovolscalem1  25683  ioombl1lem4  25731  mbfmulc2lem  25817  ismbf3d  25824  mbfsup  25834  mbfinf  25835  i1f1lem  25859  i1fmulclem  25872  mbfi1fseqlem4  25888  itg2seq  25912  ditgneg  26027  limcdif  26046  limcnlp  26048  cnplimc  26057  rolle  26160  mvth  26162  dvne0  26181  lhop1lem  26183  itgsubst  26219  mdegle0  26245  deg1leb  26263  deg1le0  26279  q1peqb  26324  coemulhi  26422  dgrlt  26434  plydivlem3  26467  vieta1lem2  26483  aannenlem1  26502  ulmres  26562  reefiso  26622  pilem3  26627  ellogdm  26815  root1eq1  26931  angpieqvdlem  27004  angpieqvdlem2  27005  quad2  27015  1cubr  27018  quart  27037  rlimcnp  27141  wilthlem2  27244  isppw  27289  dvdsflsumcom  27363  fsumvma  27388  logfac2  27392  chpchtsum  27394  dchrmulcl  27424  dchrresb  27434  bclbnd  27455  bposlem1  27459  bposlem5  27463  gausslemma2dlem0c  27533  lgsquadlem1  27555  m1lgs  27563  2lgsoddprmlem2  27584  dchrisumlem3  27666  dchrisum0lem1  27691  ltsval2  27831  noextenddif  27843  lesloe  27929  lestri3  27930  eqcuts  27989  elmade2  28062  ltadds1  28196  negsunif  28259  ltsubs1  28280  ltsubadds2d  28294  mulsproplem12  28331  ltmuls2  28375  ltmuls1d  28377  divmulsw  28397  ltdivmuls2wd  28404  oniso  28475  n0subs  28567  n0lesltp1  28570  elzn0s  28602  avglts1d  28657  avglts2d  28658  bdaypw2n0bndlem  28667  z12sge0  28687  dfz12s2  28692  elreno2  28699  tgjustr  28754  trgcgrg  28795  lnrot1  28907  islnopp  29031  elplng  29073  plngcplem  29078  ismidb  29098  islmib  29107  axsegconlem6  29283  axeuclidlem  29323  axcontlem2  29326  axcontlem4  29328  axcontlem12  29336  ausgrusgrb  29526  nb3grpr2  29744  cplgr2v  29793  umgr2v2enb1  29887  crctcsh  30184  clwwlknonwwlknonb  30468  eupth2lems  30600  nmoreltpnf  31132  isblo2  31146  nmlnogt0  31160  phoeqi  31220  ubthlem2  31234  hire  31457  normgt0  31490  ho01i  32191  ho02i  32192  hoeq1  32193  hoeq2  32194  nmopreltpnf  32232  adjeq  32298  leop  32486  leopmul2i  32498  pjnormssi  32531  pjimai  32539  jplem1  32631  mddmd2  32672  mdslmd1lem1  32688  mdslmd1lem2  32689  superpos  32717  atnssm0  32739  dmdbr5ati  32785  disjunsn  32950  fcoinvbr  32961  ofpreima  33021  funcnv5mpt  33023  suppiniseg  33042  isoun  33058  fpwrelmapffslem  33088  fpwrelmap  33089  iocinioc2  33135  xrdifh  33136  nndiffz1  33142  xdivmul  33255  cntzsnid  33409  cntrval2  33500  isarchi2  33514  isunitc  33570  erler  33594  rlocisunit  33605  elrsp  33695  lsmsnpridl  33718  lsmssass  33720  esplyind  33974  finexttrb  34064  algextdeglem6  34121  algextdeglem7  34122  smatrcl  34195  rhmpreimacnlem  34283  sqsscirc2  34308  xrmulc1cn  34329  esumfsup  34469  1stmbfm  34659  2ndmbfm  34660  mbfmcnt  34667  eulerpartlems  34759  eulerpartlemd  34765  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemsima  34915  ballotlemfrcn0  34929  reprinfz1  35018  reprdifc  35023  bnj1173  35399  fineqvnttrclse  35545  kardcard2  35587  vonf1wev  35600  vonf1owevOLD  35602  zltp1ne  35609  lfuhgr2  35619  erdszelem7  35697  erdszelem9  35699  iscvm  35759  cvmlift3lem4  35822  rexxfr3dALT  36139  fscgr  36580  seglelin  36616  btwnoutside  36625  lineunray  36647  cldbnd  36865  isfne4  36879  fneval  36891  filnetlem4  36920  nndivsub  36996  bj-gabima  37604  dfgcd3  37996  fvineqsneu  38085  wl-sbhbt  38237  wl-sbcom2d  38244  wl-sbalnae  38245  sin2h  38289  cos2h  38290  matunitlindflem1  38295  matunitlindflem2  38296  matunitlindf  38297  ptrest  38298  poimirlem3  38302  poimirlem4  38303  poimirlem22  38321  poimirlem27  38326  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  itg2addnclem  38350  itg2addnclem2  38351  itg2gt0cn  38354  iblabsnclem  38362  ftc1anclem6  38377  areacirclem2  38388  areacirclem5  38391  areacirc  38392  mettrifi  38436  drngoi  38630  eldm4  38958  exanres2  38980  disjecxrn  39089  exeupre  39168  brcoss2  39199  br1cossres2  39207  eldmcoss2  39226  eldm1cossres2  39228  brcosscnv2  39240  erimeq2  39440  disjqmap  39504  disjlem19  39581  prter3  39684  islshpat  39819  lsatnle  39846  ellkr2  39893  lshpkr  39919  lkr0f2  39963  lduallkr3  39964  lkreqN  39972  cvrval2  40076  isat3  40109  glbconN  40179  hlrelat5N  40203  cvrval4N  40216  atlt  40239  1cvrco  40274  pmaple  40563  isline2  40576  isline4N  40579  elpaddn0  40602  elpadd2at2  40609  cdlemkid4  41736  dia0  41854  cdlemm10N  41920  dibglbN  41968  dihmeetlem4preN  42108  dochkrshp3  42190  dvh4dimlem  42245  lcfl5  42298  mapdpglem3  42477  mapdheq  42530  hdmap1eq  42603  hdmapval2lem  42633  hdmapoc  42733  hlhillcs  42760  lcmineqlem18  42841  dvdsexpb  43124  renegadd  43161  resubadd  43168  redivmuld  43234  mulgt0b1d  43274  fsuppssind  43353  fz1eqin  43528  diophin  43531  jm2.19  43748  rmxdiophlem  43770  pw2f1ocnv  43792  wepwsolem  43797  gicabl  43854  idomodle  43946  onsupmaxb  43994  cantnf2  44080  tfsconcatb0  44099  tfsnfin  44107  ntrclsfveq2  44815  ntrclsss  44817  ntrclsk4  44826  extoimad  44918  radcnvrat  45052  bcc0  45078  hashomiso  45762  supxrre3rnmpt  46171  clim2f  46378  clim2f2  46412  liminfreuzlem  46544  liminfltlem  46546  xlimmnflimsup2  46594  xlimpnfliminf2  46603  xlimlimsupleliminf  46605  opprb  47796  funbrafv2b  47924  dfafn5a  47925  leaddsuble  48062  mod2addne  48135  iccpartgtprec  48197  flsqrt  48373  dfeven2  48442  dfodd3  48443  lindslinindimp2lem4  49269  snlindsntor  49279  regt1loggt0  49344  elbigo2  49360  elbigolo1  49365  fldivexpfllog2  49373  nnlog2ge0lt1  49374  blenpw2m1  49387  naryfvalelwrdf  49441  isprsd  49761  resccatlem  49879  functhinclem1  50250  thincciso  50259  thinciso  50276  isinito2lem  50304  fulltermc  50317  prstcprs  50366  oduoppcciso  50372  postc  50375  lmdran  50477  cmdlan  50478