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 223	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3bitr2d  307  3bitr2rd  308  3bitr4d  311  3bitr4rd  312  bianabs  541  mpbirand  707  sb3b  2478  sbcom3  2508  sbal1  2530  sbal2  2531  2reu4lem  4527  issn  4836  disjprg  5143  reuhypd  5424  snelpwg  5452  ordtri3  6421  ordsssuc  6474  iota1  6539  funbrfv2b  6965  dffn5  6966  feqmptdf  6978  unima  6983  dmfco  7004  fneqeql  7065  f1ompt  7130  dff13  7274  fliftcnv  7330  soisores  7346  isotr  7355  isoini  7357  caovord3  7645  releldm2  8066  fimaproj  8158  brtpos  8258  tpostpos  8269  oe1m  8581  oawordri  8586  oalimcl  8596  omlimcl  8614  omabs  8687  iserd  8769  qliftel  8838  qliftfun  8840  qliftf  8843  ecopovsym  8857  pw2f1olem  9114  mapen  9179  findcard3  9315  suppeqfsuppbi  9416  mapfien  9445  supisolem  9510  cantnflem1  9726  wemapwe  9734  rankr1clem  9857  rankr1c  9858  ranklim  9881  r1pwALT  9883  r1pwcl  9884  isfin1-2  10422  isfin1-4  10424  fin71num  10434  axdc3lem2  10488  ltmnq  11009  prlem936  11084  ltsosr  11131  ltasr  11137  xrlenlt  11323  ltxrlt  11328  letri3  11343  ne0gt0  11363  subadd  11508  ltsubadd2  11731  lesubadd2  11733  suble  11738  ltsub23  11740  ltaddpos2  11751  ltsubpos  11752  subge02  11776  ltord2  11789  leord2  11790  ltaddsublt  11887  divmul  11922  divmul3  11924  rec11r  11963  ltdiv1  12129  ltdivmul2  12142  ledivmul2  12144  ltrec  12147  ltdiv2  12151  negfi  12214  negiso  12245  nnle1eq1  12293  avgle1  12503  avgle2  12504  avgle  12505  nn0le0eq0  12551  elz2  12628  znnnlt1  12641  zleltp1  12665  difrp  13070  xrltlen  13184  dfle2  13185  xrletri3  13192  xgepnf  13203  xlemnf  13205  qbtwnre  13237  xltnegi  13254  supxrre  13365  infxrre  13374  elioo5  13440  elfz5  13552  elfzm11  13631  predfz  13689  flbi  13852  flbi2  13853  fldiv4lem1div2uz2  13872  fznnfl  13898  zmodid2  13935  2submod  13969  lt2sq  14169  le2sq  14170  sqlecan  14244  bcval5  14353  pfxsuffeqwrdeq  14732  shftfib  15107  mulre  15156  cnpart  15275  01sqrexlem6  15282  sqrmo  15286  elicc4abs  15354  abs2difabs  15369  cau4  15391  limsupgre  15513  clim2  15536  ello1mpt2  15554  lo1resb  15596  o1resb  15598  climeq  15599  climmpt2  15605  isercoll  15700  caucvgb  15712  fsumabs  15833  isumshft  15871  geomulcvg  15908  absefib  16230  dvdsval3  16290  addmulmodb  16299  dvdsabseq  16346  dvdsflip  16350  dvdsssfz1  16351  mod2eq1n2dvds  16380  ndvdsadd  16443  bitscmp  16471  smupvallem  16516  dvdssq  16600  lcmdvds  16641  ncoprmgcdgt1b  16684  isprm3  16716  isprm5  16740  phiprmpw  16809  prmdiv  16818  pc11  16913  pcz  16914  pockthlem  16938  prmreclem2  16950  prmreclem4  16952  prmreclem6  16954  1arith  16960  vdwapun  17007  rami  17048  ramcl  17062  pwsle  17538  ercpbllem  17594  invsym  17809  funcres2c  17954  latnle  18530  grpinvcnv  19036  subgacs  19191  eqger  19208  ghmqusker  19317  gexdvds2  19617  pgpfi1  19627  pgpfi  19637  lsmass  19701  lssnle  19706  lsmdisj3b  19722  lsmhash  19737  ablsubadd  19841  gsumval3lem2  19938  subgdmdprd  20068  pgpfac1lem2  20109  dvdsr02  20388  issubrg3  20616  isdomn3  20731  drngid2  20768  sdrgunit  20813  sdrgacs  20818  lssacs  20982  prmirred  21502  chrdvds  21558  chrcong  21559  chrnzr  21562  znleval  21590  znleval2  21591  cygznlem3  21605  frlmbas  21792  elfilspd  21840  lindfmm  21864  islindf4  21875  islindf5  21876  psrbaglefi  21963  coe1mul2lem1  22285  mdetunilem9  22641  isneip  23128  neiptopnei  23155  lpdifsn  23166  restopnb  23198  restopn2  23200  restdis  23201  restperf  23207  lmbr2  23282  cncls2  23296  cnprest  23312  cnprest2  23313  iscnrm2  23361  ist0-2  23367  ist1-3  23372  ishaus2  23374  cmpfi  23431  dfconn2  23442  1stccnp  23485  subislly  23504  hausmapdom  23523  tx1cn  23632  tx2cn  23633  txcnmpt  23647  txrest  23654  hauseqlcld  23669  tgqtop  23735  qtopcld  23736  ordthmeolem  23824  trfil2  23910  trfil3  23911  trnei  23915  ufildr  23954  fmfg  23972  rnelfm  23976  fmfnfm  23981  elflim  23994  flimrest  24006  cnflf  24025  cnflf2  24026  ptcmplem2  24076  ghmcnp  24138  tsmssubm  24166  iscfilu  24312  xmetgt0  24383  prdsxmetlem  24393  blcomps  24418  blcom  24419  xblpnfps  24420  xblpnf  24421  blpnf  24422  xmeter  24458  setsxms  24506  imasf1obl  24516  stdbdbl  24545  metrest  24552  metuel2  24593  dscopn  24601  xrtgioo  24841  metdstri  24886  cnmpopc  24968  iihalf2  24974  icopnfhmeo  24987  evth2  25005  lmmbr3  25307  iscau3  25325  metcld  25353  cfilucfil3  25367  srabn  25407  rrxmet  25455  minveclem4  25479  evthicc2  25508  ovolgelb  25528  shft2rab  25556  ovolshftlem1  25557  sca2rab  25560  ovolscalem1  25561  ioombl1lem4  25609  mbfmulc2lem  25695  ismbf3d  25702  mbfsup  25712  mbfinf  25713  i1f1lem  25737  i1fmulclem  25751  mbfi1fseqlem4  25767  itg2seq  25791  ditgneg  25906  limcdif  25925  limcnlp  25927  cnplimc  25936  rolle  26042  mvth  26045  dvne0  26064  lhop1lem  26066  itgsubst  26104  mdegle0  26130  deg1leb  26148  deg1le0  26164  q1peqb  26209  coemulhi  26307  dgrlt  26320  plydivlem3  26351  vieta1lem2  26367  aannenlem1  26384  ulmres  26445  reefiso  26506  pilem3  26511  ellogdm  26695  root1eq1  26812  angpieqvdlem  26885  angpieqvdlem2  26886  quad2  26896  1cubr  26899  quart  26918  rlimcnp  27022  wilthlem2  27126  isppw  27171  dvdsflsumcom  27245  fsumvma  27271  logfac2  27275  chpchtsum  27277  dchrmulcl  27307  dchrresb  27317  bclbnd  27338  bposlem1  27342  bposlem5  27346  gausslemma2dlem0c  27416  lgsquadlem1  27438  m1lgs  27446  2lgsoddprmlem2  27467  dchrisumlem3  27549  dchrisum0lem1  27574  sltval2  27715  noextenddif  27727  sleloe  27813  sletri3  27814  eqscut  27864  elmade2  27921  sltadd1  28039  negsunif  28101  sltsub1  28120  sltsubadd2d  28134  mulsproplem12  28167  sltmul2  28211  sltmul1d  28213  divsmulw  28232  sltdivmul2wd  28239  n0subs  28374  elzn0s  28398  tgjustr  28496  trgcgrg  28537  lnrot1  28645  islnopp  28761  ismidb  28800  islmib  28809  axsegconlem6  28951  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  axcontlem12  29004  ausgrusgrb  29196  nb3grpr2  29414  cplgr2v  29463  umgr2v2enb1  29558  crctcsh  29853  clwwlknonwwlknonb  30134  eupth2lems  30266  nmoreltpnf  30797  isblo2  30811  nmlnogt0  30825  phoeqi  30885  ubthlem2  30899  hire  31122  normgt0  31155  ho01i  31856  ho02i  31857  hoeq1  31858  hoeq2  31859  nmopreltpnf  31897  adjeq  31963  leop  32151  leopmul2i  32163  pjnormssi  32196  pjimai  32204  jplem1  32296  mddmd2  32337  mdslmd1lem1  32353  mdslmd1lem2  32354  superpos  32382  atnssm0  32404  dmdbr5ati  32450  disjunsn  32613  fcoinvbr  32624  ofpreima  32681  funcnv5mpt  32684  suppiniseg  32700  isoun  32716  fpwrelmapffslem  32749  fpwrelmap  32750  iocinioc2  32787  xrdifh  32788  nndiffz1  32794  xdivmul  32891  cntzsnid  33054  isarchi2  33174  erler  33251  elrsp  33379  lsmsnpridl  33405  lsmssass  33409  r1pid2OLD  33608  finexttrb  33689  algextdeglem6  33727  algextdeglem7  33728  smatrcl  33756  rhmpreimacnlem  33844  sqsscirc2  33869  xrmulc1cn  33890  esumfsup  34050  1stmbfm  34241  2ndmbfm  34242  mbfmcnt  34249  eulerpartlems  34341  eulerpartlemd  34347  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemsima  34496  ballotlemfrcn0  34510  sgn3da  34522  reprinfz1  34615  reprdifc  34620  bnj1173  34994  zltp1ne  35093  lfuhgr2  35102  erdszelem7  35181  erdszelem9  35183  iscvm  35243  cvmlift3lem4  35306  rexxfr3dALT  35623  fscgr  36061  seglelin  36097  btwnoutside  36106  lineunray  36128  cldbnd  36308  isfne4  36322  fneval  36334  filnetlem4  36363  nndivsub  36439  bj-gabima  36922  dfgcd3  37306  fvineqsneu  37393  wl-sbhbt  37534  wl-sbcom2d  37541  wl-sbalnae  37542  wl-ax11-lem8  37572  sin2h  37596  cos2h  37597  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  ptrest  37605  poimirlem3  37609  poimirlem4  37610  poimirlem22  37628  poimirlem27  37633  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem  37657  itg2addnclem2  37658  itg2gt0cn  37661  iblabsnclem  37669  ftc1anclem6  37684  areacirclem2  37695  areacirclem5  37698  areacirc  37699  mettrifi  37743  drngoi  37937  eldm4  38255  exanres2  38278  disjecxrn  38370  brcoss2  38413  br1cossres2  38421  eldmcoss2  38440  eldm1cossres2  38442  brcosscnv2  38454  erimeq2  38659  disjlem19  38782  prter3  38863  islshpat  38998  lsatnle  39025  ellkr2  39072  lshpkr  39098  lkr0f2  39142  lduallkr3  39143  lkreqN  39151  cvrval2  39255  isat3  39288  glbconN  39358  glbconNOLD  39359  hlrelat5N  39383  cvrval4N  39396  atlt  39419  1cvrco  39454  pmaple  39743  isline2  39756  isline4N  39759  elpaddn0  39782  elpadd2at2  39789  cdlemkid4  40916  dia0  41034  cdlemm10N  41100  dibglbN  41148  dihmeetlem4preN  41288  dochkrshp3  41370  dvh4dimlem  41425  lcfl5  41478  mapdpglem3  41657  mapdheq  41710  hdmap1eq  41783  hdmapval2lem  41813  hdmapoc  41913  hlhillcs  41944  lcmineqlem18  42027  dvdsexpb  42348  renegadd  42378  resubadd  42385  mulgt0b2d  42466  fsuppssind  42579  fz1eqin  42756  diophin  42759  jm2.19  42981  rmxdiophlem  43003  pw2f1ocnv  43025  wepwsolem  43030  gicabl  43087  idomodle  43179  onsupmaxb  43227  cantnf2  43314  tfsconcatb0  43333  tfsnfin  43341  ntrclsfveq2  44050  ntrclsss  44052  ntrclsk4  44061  extoimad  44153  radcnvrat  44309  bcc0  44335  supxrre3rnmpt  45378  clim2f  45591  clim2f2  45625  liminfreuzlem  45757  liminfltlem  45759  xlimmnflimsup2  45807  xlimpnfliminf2  45816  xlimlimsupleliminf  45818  opprb  46980  funbrafv2b  47108  dfafn5a  47109  leaddsuble  47246  iccpartgtprec  47344  flsqrt  47517  dfeven2  47573  dfodd3  47574  lindslinindimp2lem4  48306  snlindsntor  48316  regt1loggt0  48385  elbigo2  48401  elbigolo1  48406  fldivexpfllog2  48414  nnlog2ge0lt1  48415  blenpw2m1  48428  naryfvalelwrdf  48482  isprsd  48751  functhinclem1  48840  thincciso  48848  thinciso  48860  prstcprs  48875  oduoppcciso  48881  postc  48884