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  551  mpbirand  720  sb3b  2507  sbcom3  2537  sbal1  2559  sbal2  2560  2reu4lem  4482  issn  4795  disjprg  5103  reuhypd  5388  snelpwg  5422  ordtri3  6398  ordsssuc  6453  iota1  6516  funbrfv2b  6939  dffn5  6940  feqmptdf  6952  unima  6957  dmfco  6978  fneqeql  7042  f1ompt  7107  dff13  7254  fliftcnv  7315  soisores  7331  isotr  7340  isoini  7342  caovord3  7630  releldm2  8043  fimaproj  8136  brtpos  8236  tpostpos  8247  oe1m  8535  oawordri  8540  oalimcl  8550  omlimcl  8568  omabs  8642  iserd  8726  qliftel  8803  qliftfun  8805  qliftf  8808  ecopovsym  8822  pw2f1olem  9082  mapen  9142  findcard3  9256  tfsnfin2  9333  suppeqfsuppbi  9352  mapfien  9381  supisolem  9447  cantnflem1  9671  wemapwe  9679  rankr1clem  9805  rankr1c  9806  ranklim  9829  r1pwALT  9831  r1pwcl  9832  isfin1-2  10390  isfin1-4  10392  fin71num  10402  axdc3lem2  10456  infinfg  10577  ltmnq  10984  prlem936  11059  ltsosr  11106  ltasr  11112  xrlenlt  11301  ltxrlt  11307  letri3  11322  ne0gt0  11342  subadd  11487  ltsubadd2  11712  lesubadd2  11714  suble  11719  ltsub23  11721  ltaddpos2  11732  ltsubpos  11733  subge02  11757  ltord2  11770  leord2  11771  ltaddsublt  11868  divmul  11902  divmul3  11904  rec11r  11941  ltdiv1  12106  ltdivmul2  12119  ledivmul2  12121  ltrec  12124  ltdiv2  12128  negfi  12191  negiso  12222  nnle1eq1  12293  avgle1  12511  avgle2  12512  avgle  12513  nn0le0eq0  12559  elz2  12636  znnnlt1  12648  zleltp1  12672  difrp  13084  xrltlen  13199  dfle2  13200  xrletri3  13207  xgepnf  13219  xlemnf  13221  qbtwnre  13253  xltnegi  13270  supxrre  13381  infxrre  13391  elioo5  13458  elfz5  13572  elfzm11  13652  predfz  13710  flbi  13879  flbi2  13880  fldiv4lem1div2uz2  13899  fznnfl  13925  zmodid2  13962  2submod  13998  lt2sq  14199  le2sq  14200  sqlecan  14275  bcval5  14384  pfxsuffeqwrdeq  14769  shftfib  15147  sgn3da  15176  mulre  15210  cnpart  15329  01sqrexlem6  15336  sqrmo  15340  elicc4abs  15409  abs2difabs  15424  cau4  15446  limsupgre  15570  clim2  15593  ello1mpt2  15611  lo1resb  15653  o1resb  15655  climeq  15656  climmpt2  15662  isercoll  15757  caucvgb  15769  fsumabs  15890  isumshft  15930  geomulcvg  15967  absefib  16290  dvdsval3  16350  addmulmodb  16359  dvdsabseq  16407  dvdsflip  16411  dvdsssfz1  16412  mod2eq1n2dvds  16441  ndvdsadd  16504  bitscmp  16532  smupvallem  16577  dvdssq  16661  lcmdvds  16702  ncoprmgcdgt1b  16745  isprm3  16777  isprm5  16802  phiprmpw  16871  prmdiv  16880  pc11  16976  pcz  16977  pockthlem  17001  prmreclem2  17013  prmreclem4  17015  prmreclem6  17017  1arith  17023  vdwapun  17070  rami  17111  ramcl  17125  pwsle  17582  ercpbllem  17638  invsym  17855  funcres2c  17996  latnle  18565  grpinvcnv  19131  subgacs  19285  eqger  19304  ghmqusker  19415  gexdvds2  19713  pgpfi1  19723  pgpfi  19733  lsmass  19797  lssnle  19802  lsmdisj3b  19818  lsmhash  19833  ablsubadd  19937  gsumval3lem2  20034  subgdmdprd  20164  pgpfac1lem2  20205  dvdsr02  20514  issubrg3  20763  isdomn3  20877  drngid2  20920  sdrgunit  20963  sdrgacs  20968  lssacs  21152  prmirred  21688  chrdvds  21740  chrcong  21741  chrnzr  21744  znleval  21768  znleval2  21769  cygznlem3  21783  frlmbas  21969  elfilspd  22017  lindfmm  22041  islindf4  22052  islindf5  22053  psrbaglefi  22142  coe1mul2lem1  22494  mdetunilem9  22843  matunitlindflem1  22902  matunitlindflem2  22903  matunitlindf  22904  isneip  23331  neiptopnei  23358  lpdifsn  23369  restopnb  23401  restopn2  23403  restdis  23404  restperf  23410  lmbr2  23485  cncls2  23499  cnprest  23515  cnprest2  23516  iscnrm2  23564  ist0-2  23570  ist1-3  23575  ishaus2  23577  cmpfi  23634  dfconn2  23645  1stccnp  23689  subislly  23708  hausmapdom  23727  tx1cn  23836  tx2cn  23837  txcnmpt  23851  txrest  23858  hauseqlcld  23873  tgqtop  23939  qtopcld  23940  ordthmeolem  24028  trfil2  24114  trfil3  24115  trnei  24119  ufildr  24158  fmfg  24176  rnelfm  24180  fmfnfm  24185  elflim  24198  flimrest  24210  cnflf  24229  cnflf2  24230  ptcmplem2  24280  ghmcnp  24342  tsmssubm  24370  iscfilu  24514  xmetgt0  24585  prdsxmetlem  24595  blcomps  24620  blcom  24621  xblpnfps  24622  xblpnf  24623  blpnf  24624  xmeter  24660  setsxms  24706  imasf1obl  24715  stdbdbl  24744  metrest  24751  metuel2  24792  dscopn  24800  xrtgioo  25034  metdstri  25079  cnmpopc  25157  iihalf2  25162  icopnfhmeo  25172  evth2  25189  lmmbr3  25489  iscau3  25507  metcld  25535  cfilucfil3  25549  srabn  25589  rrxmet  25637  minveclem4  25661  evthicc2  25689  ovolgelb  25709  shft2rab  25737  ovolshftlem1  25738  sca2rab  25741  ovolscalem1  25742  ioombl1lem4  25790  mbfmulc2lem  25876  ismbf3d  25883  mbfsup  25893  mbfinf  25894  i1f1lem  25918  i1fmulclem  25931  mbfi1fseqlem4  25947  itg2seq  25971  ditgneg  26086  limcdif  26105  limcnlp  26107  cnplimc  26116  rolle  26219  mvth  26221  dvne0  26240  lhop1lem  26242  itgsubst  26278  mdegle0  26304  deg1leb  26322  deg1le0  26338  q1peqb  26383  coemulhi  26481  dgrlt  26493  plydivlem3  26526  vieta1lem2  26542  aannenlem1  26561  ulmres  26621  reefiso  26681  pilem3  26686  ellogdm  26874  root1eq1  26990  angpieqvdlem  27063  angpieqvdlem2  27064  quad2  27074  1cubr  27077  quart  27096  rlimcnp  27200  wilthlem2  27303  isppw  27348  dvdsflsumcom  27422  fsumvma  27447  logfac2  27451  chpchtsum  27453  dchrmulcl  27483  dchrresb  27493  bclbnd  27514  bposlem1  27518  bposlem5  27522  gausslemma2dlem0c  27592  lgsquadlem1  27614  m1lgs  27622  2lgsoddprmlem2  27643  dchrisumlem3  27725  dchrisum0lem1  27750  ltsval2  27890  noextenddif  27902  lesloe  27988  lestri3  27989  eqcuts  28048  elmade2  28121  ltadds1  28255  negsunif  28318  ltsubs1  28339  ltsubadds2d  28353  mulsproplem12  28390  ltmuls2  28434  ltmuls1d  28436  divmulsw  28456  ltdivmuls2wd  28463  oniso  28534  n0subs  28626  n0lesltp1  28629  elzn0s  28661  avglts1d  28716  avglts2d  28717  bdaypw2n0bndlem  28726  z12sge0  28746  dfz12s2  28751  elreno2  28758  tgjustr  28813  trgcgrg  28855  lnrot1  28968  islnopp  29092  elplng  29135  plngcplem  29140  ismidb  29160  islmib  29169  axsegconlem6  29365  axeuclidlem  29405  axcontlem2  29408  axcontlem4  29410  axcontlem12  29418  lfuhgr2  29592  ausgrusgrb  29611  nb3grpr2  29829  cplgr2v  29878  umgr2v2enb1  29972  crctcsh  30278  clwwlknonwwlknonb  30562  eupth2lems  30704  nmoreltpnf  31236  isblo2  31250  nmlnogt0  31264  phoeqi  31324  ubthlem2  31338  hire  31561  normgt0  31594  ho01i  32295  ho02i  32296  hoeq1  32297  hoeq2  32298  nmopreltpnf  32336  adjeq  32402  leop  32590  leopmul2i  32602  pjnormssi  32635  pjimai  32643  jplem1  32735  mddmd2  32776  mdslmd1lem1  32792  mdslmd1lem2  32793  superpos  32821  atnssm0  32843  dmdbr5ati  32889  disjunsn  33054  fcoinvbr  33065  ofpreima  33125  funcnv5mpt  33127  suppiniseg  33145  isoun  33161  fpwrelmapffslem  33190  fpwrelmap  33191  iocinioc2  33237  xrdifh  33238  nndiffz1  33244  xdivmul  33357  cntzsnid  33507  cntrval2  33598  isarchi2  33612  isunitc  33668  erler  33692  rlocisunit  33703  elrsp  33793  lsmsnpridl  33816  lsmssass  33818  esplyind  34072  finexttrb  34162  algextdeglem6  34219  algextdeglem7  34220  smatrcl  34293  rhmpreimacnlem  34381  sqsscirc2  34406  xrmulc1cn  34427  esumfsup  34567  1stmbfm  34758  2ndmbfm  34759  mbfmcnt  34766  eulerpartlems  34858  eulerpartlemd  34864  ballotlemfc0  34991  ballotlemfcc  34992  ballotlemsima  35014  ballotlemfrcn0  35028  reprinfz1  35117  reprdifc  35122  bnj1173  35498  fineqvnttrclse  35637  kardcard2  35679  vonf1wev  35692  vonf1owevOLD  35694  zltp1ne  35701  erdszelem7  35763  erdszelem9  35765  iscvm  35825  cvmlift3lem4  35888  rexxfr3dALT  36205  fscgr  36647  seglelin  36683  btwnoutside  36692  lineunray  36714  cldbnd  36932  isfne4  36946  fneval  36958  filnetlem4  36987  nndivsub  37063  bj-gabima  37671  dfgcd3  38063  fvineqsneu  38152  wl-sbhbt  38304  wl-sbcom2d  38311  wl-sbalnae  38312  sin2h  38351  cos2h  38352  ptrest  38355  poimirlem3  38359  poimirlem4  38360  poimirlem22  38378  poimirlem27  38383  mblfinlem3  38395  mblfinlem4  38396  ismblfin  38397  itg2addnclem  38407  itg2addnclem2  38408  itg2gt0cn  38411  iblabsnclem  38419  ftc1anclem6  38434  areacirclem2  38445  areacirclem5  38448  areacirc  38449  mettrifi  38494  drngoi  38688  eldm4  39016  exanres2  39038  disjecxrn  39147  exeupre  39226  brcoss2  39257  br1cossres2  39265  eldmcoss2  39284  eldm1cossres2  39286  brcosscnv2  39298  erimeq2  39498  disjqmap  39562  disjlem19  39639  prter3  39742  islshpat  39877  lsatnle  39904  ellkr2  39951  lshpkr  39977  lkr0f2  40021  lduallkr3  40022  lkreqN  40030  cvrval2  40134  isat3  40167  glbconN  40237  hlrelat5N  40261  cvrval4N  40274  atlt  40297  1cvrco  40332  pmaple  40621  isline2  40634  isline4N  40637  elpaddn0  40660  elpadd2at2  40667  cdlemkid4  41794  dia0  41912  cdlemm10N  41978  dibglbN  42026  dihmeetlem4preN  42166  dochkrshp3  42248  dvh4dimlem  42303  lcfl5  42356  mapdpglem3  42535  mapdheq  42588  hdmap1eq  42661  hdmapval2lem  42691  hdmapoc  42791  hlhillcs  42818  lcmineqlem18  42899  dvdsexpb  43197  renegadd  43234  resubadd  43241  redivmuld  43307  mulgt0b1d  43347  fsuppssind  43426  fz1eqin  43601  diophin  43604  jm2.19  43821  rmxdiophlem  43843  pw2f1ocnv  43865  wepwsolem  43870  gicabl  43927  idomodle  44019  onsupmaxb  44067  cantnf2  44153  tfsconcatb0  44172  tfsnfin  44180  ntrclsfveq2  44888  ntrclsss  44890  ntrclsk4  44899  extoimad  44991  radcnvrat  45125  bcc0  45151  hashomiso  45835  supxrre3rnmpt  46244  clim2f  46451  clim2f2  46485  liminfreuzlem  46617  liminfltlem  46619  xlimmnflimsup2  46667  xlimpnfliminf2  46676  xlimlimsupleliminf  46678  opprb  47906  funbrafv2b  48034  dfafn5a  48035  leaddsuble  48172  mod2addne  48245  iccpartgtprec  48307  flsqrt  48483  dfeven2  48552  dfodd3  48553  lindslinindimp2lem4  49378  snlindsntor  49388  regt1loggt0  49453  elbigo2  49469  elbigolo1  49474  fldivexpfllog2  49482  nnlog2ge0lt1  49483  blenpw2m1  49496  naryfvalelwrdf  49550  isprsd  49868  resccatlem  49986  functhinclem1  50357  thincciso  50366  thinciso  50383  isinito2lem  50411  fulltermc  50424  prstcprs  50473  oduoppcciso  50479  postc  50482  lmdran  50584  cmdlan  50585