Theorem bitr4d 281

Description: Deduction form of bitr4i 277. (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 278	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  306  3bitr2rd  307  3bitr4d  310  3bitr4rd  311  bianabs  540  mpbirand  705  sb3b  2469  sbcom3  2499  sbal1  2521  sbal2  2522  2reu4lem  4526  issn  4834  disjprgw  5143  disjprg  5144  reuhypd  5418  snelpwg  5443  ordtri3  6405  ordsssuc  6458  iota1  6524  funbrfv2b  6953  dffn5  6954  feqmptdf  6966  unima  6970  dmfco  6991  fneqeql  7052  f1ompt  7118  dff13  7263  fliftcnv  7316  soisores  7332  isotr  7341  isoini  7343  caovord3  7632  releldm2  8046  fimaproj  8138  brtpos  8239  tpostpos  8250  oe1m  8564  oawordri  8569  oalimcl  8579  omlimcl  8597  omabs  8670  iserd  8749  qliftel  8817  qliftfun  8819  qliftf  8822  ecopovsym  8836  pw2f1olem  9099  mapen  9164  findcard3  9308  suppeqfsuppbi  9402  mapfien  9431  supisolem  9496  cantnflem1  9712  wemapwe  9720  rankr1clem  9843  rankr1c  9844  ranklim  9867  r1pwALT  9869  r1pwcl  9870  isfin1-2  10408  isfin1-4  10410  fin71num  10420  axdc3lem2  10474  ltmnq  10995  prlem936  11070  ltsosr  11117  ltasr  11123  xrlenlt  11309  ltxrlt  11314  letri3  11329  ne0gt0  11349  subadd  11493  ltsubadd2  11715  lesubadd2  11717  suble  11722  ltsub23  11724  ltaddpos2  11735  ltsubpos  11736  subge02  11760  ltord2  11773  leord2  11774  ltaddsublt  11871  divmul  11905  divmul3  11907  rec11r  11943  ltdiv1  12108  ltdivmul2  12121  ledivmul2  12123  ltrec  12126  ltdiv2  12130  negfi  12193  negiso  12224  nnle1eq1  12272  avgle1  12482  avgle2  12483  avgle  12484  nn0le0eq0  12530  elz2  12606  znnnlt1  12619  zleltp1  12643  difrp  13044  xrltlen  13157  dfle2  13158  xrletri3  13165  xgepnf  13176  xlemnf  13178  qbtwnre  13210  xltnegi  13227  supxrre  13338  infxrre  13347  elioo5  13413  elfz5  13525  elfzm11  13604  predfz  13658  flbi  13813  flbi2  13814  fldiv4lem1div2uz2  13833  fznnfl  13859  zmodid2  13896  2submod  13929  lt2sq  14129  le2sq  14130  sqlecan  14204  bcval5  14309  pfxsuffeqwrdeq  14680  shftfib  15051  mulre  15100  cnpart  15219  01sqrexlem6  15226  sqrmo  15230  elicc4abs  15298  abs2difabs  15313  cau4  15335  limsupgre  15457  clim2  15480  ello1mpt2  15498  lo1resb  15540  o1resb  15542  climeq  15543  climmpt2  15549  isercoll  15646  caucvgb  15658  fsumabs  15779  isumshft  15817  geomulcvg  15854  absefib  16174  dvdsval3  16234  dvdsabseq  16289  dvdsflip  16293  dvdsssfz1  16294  mod2eq1n2dvds  16323  ndvdsadd  16386  bitscmp  16412  smupvallem  16457  dvdssq  16537  lcmdvds  16578  ncoprmgcdgt1b  16621  isprm3  16653  isprm5  16677  phiprmpw  16744  prmdiv  16753  pc11  16848  pcz  16849  pockthlem  16873  prmreclem2  16885  prmreclem4  16887  prmreclem6  16889  1arith  16895  vdwapun  16942  rami  16983  ramcl  16997  pwsle  17473  ercpbllem  17529  invsym  17744  funcres2c  17889  latnle  18464  grpinvcnv  18967  subgacs  19120  eqger  19137  ghmqusker  19242  gexdvds2  19544  pgpfi1  19554  pgpfi  19564  lsmass  19628  lssnle  19633  lsmdisj3b  19649  lsmhash  19664  ablsubadd  19768  gsumval3lem2  19865  subgdmdprd  19995  pgpfac1lem2  20036  dvdsr02  20315  issubrg3  20543  drngid2  20649  sdrgunit  20688  sdrgacs  20693  lssacs  20855  isdomn3  21252  prmirred  21404  chrdvds  21460  chrcong  21461  chrnzr  21464  znleval  21492  znleval2  21493  cygznlem3  21507  frlmbas  21693  elfilspd  21741  lindfmm  21765  islindf4  21776  islindf5  21777  psrbaglefi  21869  psrbaglefiOLD  21870  coe1mul2lem1  22195  mdetunilem9  22552  isneip  23039  neiptopnei  23066  lpdifsn  23077  restopnb  23109  restopn2  23111  restdis  23112  restperf  23118  lmbr2  23193  cncls2  23207  cnprest  23223  cnprest2  23224  iscnrm2  23272  ist0-2  23278  ist1-3  23283  ishaus2  23285  cmpfi  23342  dfconn2  23353  1stccnp  23396  subislly  23415  hausmapdom  23434  tx1cn  23543  tx2cn  23544  txcnmpt  23558  txrest  23565  hauseqlcld  23580  tgqtop  23646  qtopcld  23647  ordthmeolem  23735  trfil2  23821  trfil3  23822  trnei  23826  ufildr  23865  fmfg  23883  rnelfm  23887  fmfnfm  23892  elflim  23905  flimrest  23917  cnflf  23936  cnflf2  23937  ptcmplem2  23987  ghmcnp  24049  tsmssubm  24077  iscfilu  24223  xmetgt0  24294  prdsxmetlem  24304  blcomps  24329  blcom  24330  xblpnfps  24331  xblpnf  24332  blpnf  24333  xmeter  24369  setsxms  24417  imasf1obl  24427  stdbdbl  24456  metrest  24463  metuel2  24504  dscopn  24512  xrtgioo  24752  metdstri  24797  cnmpopc  24879  iihalf2  24885  icopnfhmeo  24898  evth2  24916  lmmbr3  25218  iscau3  25236  metcld  25264  cfilucfil3  25278  srabn  25318  rrxmet  25366  minveclem4  25390  evthicc2  25419  ovolgelb  25439  shft2rab  25467  ovolshftlem1  25468  sca2rab  25471  ovolscalem1  25472  ioombl1lem4  25520  mbfmulc2lem  25606  ismbf3d  25613  mbfsup  25623  mbfinf  25624  i1f1lem  25648  i1fmulclem  25662  mbfi1fseqlem4  25678  itg2seq  25702  ditgneg  25816  limcdif  25835  limcnlp  25837  cnplimc  25846  rolle  25952  mvth  25955  dvne0  25974  lhop1lem  25976  itgsubst  26014  mdegle0  26043  deg1leb  26061  deg1le0  26077  q1peqb  26121  coemulhi  26218  dgrlt  26231  plydivlem3  26260  vieta1lem2  26276  aannenlem1  26293  ulmres  26354  reefiso  26415  pilem3  26420  ellogdm  26603  root1eq1  26720  angpieqvdlem  26790  angpieqvdlem2  26791  quad2  26801  1cubr  26804  quart  26823  rlimcnp  26927  wilthlem2  27031  isppw  27076  dvdsflsumcom  27150  fsumvma  27176  logfac2  27180  chpchtsum  27182  dchrmulcl  27212  dchrresb  27222  bclbnd  27243  bposlem1  27247  bposlem5  27251  gausslemma2dlem0c  27321  lgsquadlem1  27343  m1lgs  27351  2lgsoddprmlem2  27372  dchrisumlem3  27454  dchrisum0lem1  27479  sltval2  27619  noextenddif  27631  sleloe  27717  sletri3  27718  eqscut  27768  elmade2  27825  sltadd1  27939  negsunif  27997  sltsub1  28016  sltsubadd2d  28030  mulsproplem12  28061  sltmul2  28105  sltmul1d  28107  divsmulw  28126  sltdivmul2wd  28133  n0subs  28259  elzn0s  28275  tgjustr  28334  trgcgrg  28375  lnrot1  28483  islnopp  28599  ismidb  28638  islmib  28647  axsegconlem6  28789  axeuclidlem  28829  axcontlem2  28832  axcontlem4  28834  axcontlem12  28842  ausgrusgrb  29034  nb3grpr2  29252  cplgr2v  29301  umgr2v2enb1  29396  crctcsh  29691  clwwlknonwwlknonb  29972  eupth2lems  30104  nmoreltpnf  30635  isblo2  30649  nmlnogt0  30663  phoeqi  30723  ubthlem2  30737  hire  30960  normgt0  30993  ho01i  31694  ho02i  31695  hoeq1  31696  hoeq2  31697  nmopreltpnf  31735  adjeq  31801  leop  31989  leopmul2i  32001  pjnormssi  32034  pjimai  32042  jplem1  32134  mddmd2  32175  mdslmd1lem1  32191  mdslmd1lem2  32192  superpos  32220  atnssm0  32242  dmdbr5ati  32288  disjunsn  32441  fcoinvbr  32452  ofpreima  32508  funcnv5mpt  32511  suppiniseg  32523  isoun  32538  fpwrelmapffslem  32571  fpwrelmap  32572  iocinioc2  32604  xrdifh  32605  nndiffz1  32611  xdivmul  32705  cntzsnid  32832  isarchi2  32950  erler  33019  elrsp  33145  lsmsnpridl  33169  lsmssass  33173  r1pid2  33349  finexttrb  33424  algextdeglem6  33460  algextdeglem7  33461  smatrcl  33467  rhmpreimacnlem  33555  sqsscirc2  33580  xrmulc1cn  33601  esumfsup  33759  1stmbfm  33950  2ndmbfm  33951  mbfmcnt  33958  eulerpartlems  34050  eulerpartlemd  34056  ballotlemfc0  34182  ballotlemfcc  34183  ballotlemsima  34205  ballotlemfrcn0  34219  sgn3da  34231  reprinfz1  34324  reprdifc  34329  bnj1173  34703  zltp1ne  34789  lfuhgr2  34798  erdszelem7  34877  erdszelem9  34879  iscvm  34939  cvmlift3lem4  35002  fscgr  35746  seglelin  35782  btwnoutside  35791  lineunray  35813  cldbnd  35880  isfne4  35894  fneval  35906  filnetlem4  35935  nndivsub  36011  bj-gabima  36488  dfgcd3  36873  fvineqsneu  36960  wl-sbhbt  37091  wl-sbcom2d  37098  wl-sbalnae  37099  wl-ax11-lem8  37129  sin2h  37153  cos2h  37154  matunitlindflem1  37159  matunitlindflem2  37160  matunitlindf  37161  ptrest  37162  poimirlem3  37166  poimirlem4  37167  poimirlem22  37185  poimirlem27  37190  mblfinlem3  37202  mblfinlem4  37203  ismblfin  37204  itg2addnclem  37214  itg2addnclem2  37215  itg2gt0cn  37218  iblabsnclem  37226  ftc1anclem6  37241  areacirclem2  37252  areacirclem5  37255  areacirc  37256  mettrifi  37300  drngoi  37494  eldm4  37815  exanres2  37838  disjecxrn  37930  brcoss2  37973  br1cossres2  37981  eldmcoss2  38000  eldm1cossres2  38002  brcosscnv2  38014  erimeq2  38219  disjlem19  38342  prter3  38423  islshpat  38558  lsatnle  38585  ellkr2  38632  lshpkr  38658  lkr0f2  38702  lduallkr3  38703  lkreqN  38711  cvrval2  38815  isat3  38848  glbconN  38918  glbconNOLD  38919  hlrelat5N  38943  cvrval4N  38956  atlt  38979  1cvrco  39014  pmaple  39303  isline2  39316  isline4N  39319  elpaddn0  39342  elpadd2at2  39349  cdlemkid4  40476  dia0  40594  cdlemm10N  40660  dibglbN  40708  dihmeetlem4preN  40848  dochkrshp3  40930  dvh4dimlem  40985  lcfl5  41038  mapdpglem3  41217  mapdheq  41270  hdmap1eq  41343  hdmapval2lem  41373  hdmapoc  41473  hlhillcs  41504  lcmineqlem18  41586  fsuppssind  41891  dvdsexpb  41967  renegadd  41992  resubadd  41999  mulgt0b2d  42080  fz1eqin  42254  diophin  42257  jm2.19  42479  rmxdiophlem  42501  pw2f1ocnv  42523  wepwsolem  42531  gicabl  42588  idomodle  42684  onsupmaxb  42732  cantnf2  42819  tfsconcatb0  42838  tfsnfin  42846  ntrclsfveq2  43556  ntrclsss  43558  ntrclsk4  43567  extoimad  43659  radcnvrat  43816  bcc0  43842  supxrre3rnmpt  44874  clim2f  45087  clim2f2  45121  liminfreuzlem  45253  liminfltlem  45255  xlimmnflimsup2  45303  xlimpnfliminf2  45312  xlimlimsupleliminf  45314  opprb  46476  funbrafv2b  46602  dfafn5a  46603  leaddsuble  46740  iccpartgtprec  46823  flsqrt  46996  dfeven2  47052  dfodd3  47053  lindslinindimp2lem4  47641  snlindsntor  47651  regt1loggt0  47721  elbigo2  47737  elbigolo1  47742  fldivexpfllog2  47750  nnlog2ge0lt1  47751  blenpw2m1  47764  naryfvalelwrdf  47818  isprsd  48086  functhinclem1  48159  thincciso  48167  thinciso  48178  prstcprs  48193  postc  48200