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  2474  sbcom3  2504  sbal1  2526  sbal2  2527  2reu4lem  4475  issn  4786  disjprg  5091  reuhypd  5361  snelpwg  5389  ordtri3  6347  ordsssuc  6402  iota1  6465  funbrfv2b  6884  dffn5  6885  feqmptdf  6897  unima  6902  dmfco  6923  fneqeql  6984  f1ompt  7049  dff13  7195  fliftcnv  7252  soisores  7268  isotr  7277  isoini  7279  caovord3  7566  releldm2  7985  fimaproj  8075  brtpos  8175  tpostpos  8186  oe1m  8470  oawordri  8475  oalimcl  8485  omlimcl  8503  omabs  8576  iserd  8658  qliftel  8734  qliftfun  8736  qliftf  8739  ecopovsym  8753  pw2f1olem  9005  mapen  9065  findcard3  9187  suppeqfsuppbi  9288  mapfien  9317  supisolem  9383  cantnflem1  9604  wemapwe  9612  rankr1clem  9735  rankr1c  9736  ranklim  9759  r1pwALT  9761  r1pwcl  9762  isfin1-2  10298  isfin1-4  10300  fin71num  10310  axdc3lem2  10364  ltmnq  10885  prlem936  10960  ltsosr  11007  ltasr  11013  xrlenlt  11199  ltxrlt  11204  letri3  11219  ne0gt0  11239  subadd  11384  ltsubadd2  11609  lesubadd2  11611  suble  11616  ltsub23  11618  ltaddpos2  11629  ltsubpos  11630  subge02  11654  ltord2  11667  leord2  11668  ltaddsublt  11765  divmul  11800  divmul3  11802  rec11r  11841  ltdiv1  12007  ltdivmul2  12020  ledivmul2  12022  ltrec  12025  ltdiv2  12029  negfi  12092  negiso  12123  nnle1eq1  12176  avgle1  12382  avgle2  12383  avgle  12384  nn0le0eq0  12430  elz2  12507  znnnlt1  12520  zleltp1  12544  difrp  12951  xrltlen  13066  dfle2  13067  xrletri3  13074  xgepnf  13085  xlemnf  13087  qbtwnre  13119  xltnegi  13136  supxrre  13247  infxrre  13257  elioo5  13324  elfz5  13437  elfzm11  13516  predfz  13574  flbi  13738  flbi2  13739  fldiv4lem1div2uz2  13758  fznnfl  13784  zmodid2  13821  2submod  13857  lt2sq  14058  le2sq  14059  sqlecan  14134  bcval5  14243  pfxsuffeqwrdeq  14622  shftfib  14997  mulre  15046  cnpart  15165  01sqrexlem6  15172  sqrmo  15176  elicc4abs  15245  abs2difabs  15260  cau4  15282  limsupgre  15406  clim2  15429  ello1mpt2  15447  lo1resb  15489  o1resb  15491  climeq  15492  climmpt2  15498  isercoll  15593  caucvgb  15605  fsumabs  15726  isumshft  15764  geomulcvg  15801  absefib  16125  dvdsval3  16185  addmulmodb  16194  dvdsabseq  16242  dvdsflip  16246  dvdsssfz1  16247  mod2eq1n2dvds  16276  ndvdsadd  16339  bitscmp  16367  smupvallem  16412  dvdssq  16496  lcmdvds  16537  ncoprmgcdgt1b  16580  isprm3  16612  isprm5  16636  phiprmpw  16705  prmdiv  16714  pc11  16810  pcz  16811  pockthlem  16835  prmreclem2  16847  prmreclem4  16849  prmreclem6  16851  1arith  16857  vdwapun  16904  rami  16945  ramcl  16959  pwsle  17414  ercpbllem  17470  invsym  17687  funcres2c  17828  latnle  18397  grpinvcnv  18903  subgacs  19058  eqger  19075  ghmqusker  19184  gexdvds2  19482  pgpfi1  19492  pgpfi  19502  lsmass  19566  lssnle  19571  lsmdisj3b  19587  lsmhash  19602  ablsubadd  19706  gsumval3lem2  19803  subgdmdprd  19933  pgpfac1lem2  19974  dvdsr02  20275  issubrg3  20503  isdomn3  20618  drngid2  20655  sdrgunit  20699  sdrgacs  20704  lssacs  20888  prmirred  21399  chrdvds  21451  chrcong  21452  chrnzr  21455  znleval  21479  znleval2  21480  cygznlem3  21494  frlmbas  21680  elfilspd  21728  lindfmm  21752  islindf4  21763  islindf5  21764  psrbaglefi  21851  coe1mul2lem1  22169  mdetunilem9  22523  isneip  23008  neiptopnei  23035  lpdifsn  23046  restopnb  23078  restopn2  23080  restdis  23081  restperf  23087  lmbr2  23162  cncls2  23176  cnprest  23192  cnprest2  23193  iscnrm2  23241  ist0-2  23247  ist1-3  23252  ishaus2  23254  cmpfi  23311  dfconn2  23322  1stccnp  23365  subislly  23384  hausmapdom  23403  tx1cn  23512  tx2cn  23513  txcnmpt  23527  txrest  23534  hauseqlcld  23549  tgqtop  23615  qtopcld  23616  ordthmeolem  23704  trfil2  23790  trfil3  23791  trnei  23795  ufildr  23834  fmfg  23852  rnelfm  23856  fmfnfm  23861  elflim  23874  flimrest  23886  cnflf  23905  cnflf2  23906  ptcmplem2  23956  ghmcnp  24018  tsmssubm  24046  iscfilu  24191  xmetgt0  24262  prdsxmetlem  24272  blcomps  24297  blcom  24298  xblpnfps  24299  xblpnf  24300  blpnf  24301  xmeter  24337  setsxms  24383  imasf1obl  24392  stdbdbl  24421  metrest  24428  metuel2  24469  dscopn  24477  xrtgioo  24711  metdstri  24756  cnmpopc  24838  iihalf2  24844  icopnfhmeo  24857  evth2  24875  lmmbr3  25176  iscau3  25194  metcld  25222  cfilucfil3  25236  srabn  25276  rrxmet  25324  minveclem4  25348  evthicc2  25377  ovolgelb  25397  shft2rab  25425  ovolshftlem1  25426  sca2rab  25429  ovolscalem1  25430  ioombl1lem4  25478  mbfmulc2lem  25564  ismbf3d  25571  mbfsup  25581  mbfinf  25582  i1f1lem  25606  i1fmulclem  25619  mbfi1fseqlem4  25635  itg2seq  25659  ditgneg  25774  limcdif  25793  limcnlp  25795  cnplimc  25804  rolle  25910  mvth  25913  dvne0  25932  lhop1lem  25934  itgsubst  25972  mdegle0  25998  deg1leb  26016  deg1le0  26032  q1peqb  26077  coemulhi  26175  dgrlt  26188  plydivlem3  26219  vieta1lem2  26235  aannenlem1  26252  ulmres  26313  reefiso  26374  pilem3  26379  ellogdm  26564  root1eq1  26681  angpieqvdlem  26754  angpieqvdlem2  26755  quad2  26765  1cubr  26768  quart  26787  rlimcnp  26891  wilthlem2  26995  isppw  27040  dvdsflsumcom  27114  fsumvma  27140  logfac2  27144  chpchtsum  27146  dchrmulcl  27176  dchrresb  27186  bclbnd  27207  bposlem1  27211  bposlem5  27215  gausslemma2dlem0c  27285  lgsquadlem1  27307  m1lgs  27315  2lgsoddprmlem2  27336  dchrisumlem3  27418  dchrisum0lem1  27443  sltval2  27584  noextenddif  27596  sleloe  27682  sletri3  27683  eqscut  27734  elmade2  27800  sltadd1  27922  negsunif  27984  sltsub1  28003  sltsubadd2d  28017  mulsproplem12  28053  sltmul2  28097  sltmul1d  28099  divsmulw  28119  sltdivmul2wd  28126  onsiso  28192  n0subs  28276  n0sleltp1  28279  elzn0s  28309  avgslt1d  28362  avgslt2d  28363  zs12ge0  28378  tgjustr  28437  trgcgrg  28478  lnrot1  28586  islnopp  28702  ismidb  28741  islmib  28750  axsegconlem6  28885  axeuclidlem  28925  axcontlem2  28928  axcontlem4  28930  axcontlem12  28938  ausgrusgrb  29128  nb3grpr2  29346  cplgr2v  29395  umgr2v2enb1  29490  crctcsh  29787  clwwlknonwwlknonb  30068  eupth2lems  30200  nmoreltpnf  30731  isblo2  30745  nmlnogt0  30759  phoeqi  30819  ubthlem2  30833  hire  31056  normgt0  31089  ho01i  31790  ho02i  31791  hoeq1  31792  hoeq2  31793  nmopreltpnf  31831  adjeq  31897  leop  32085  leopmul2i  32097  pjnormssi  32130  pjimai  32138  jplem1  32230  mddmd2  32271  mdslmd1lem1  32287  mdslmd1lem2  32288  superpos  32316  atnssm0  32338  dmdbr5ati  32384  disjunsn  32556  fcoinvbr  32567  ofpreima  32622  funcnv5mpt  32625  suppiniseg  32642  isoun  32658  fpwrelmapffslem  32688  fpwrelmap  32689  iocinioc2  32735  xrdifh  32736  nndiffz1  32742  sgn3da  32792  xdivmul  32878  cntzsnid  33035  cntrval2  33126  isarchi2  33137  erler  33215  elrsp  33319  lsmsnpridl  33345  lsmssass  33349  r1pid2OLD  33550  finexttrb  33636  algextdeglem6  33688  algextdeglem7  33689  smatrcl  33762  rhmpreimacnlem  33850  sqsscirc2  33875  xrmulc1cn  33896  esumfsup  34036  1stmbfm  34227  2ndmbfm  34228  mbfmcnt  34235  eulerpartlems  34327  eulerpartlemd  34333  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemsima  34483  ballotlemfrcn0  34497  reprinfz1  34589  reprdifc  34594  bnj1173  34968  vonf1owev  35080  zltp1ne  35082  lfuhgr2  35091  erdszelem7  35169  erdszelem9  35171  iscvm  35231  cvmlift3lem4  35294  rexxfr3dALT  35611  fscgr  36053  seglelin  36089  btwnoutside  36098  lineunray  36120  cldbnd  36299  isfne4  36313  fneval  36325  filnetlem4  36354  nndivsub  36430  bj-gabima  36913  dfgcd3  37297  fvineqsneu  37384  wl-sbhbt  37527  wl-sbcom2d  37534  wl-sbalnae  37535  wl-ax11-lem8  37565  sin2h  37589  cos2h  37590  matunitlindflem1  37595  matunitlindflem2  37596  matunitlindf  37597  ptrest  37598  poimirlem3  37602  poimirlem4  37603  poimirlem22  37621  poimirlem27  37626  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  itg2addnclem  37650  itg2addnclem2  37651  itg2gt0cn  37654  iblabsnclem  37662  ftc1anclem6  37677  areacirclem2  37688  areacirclem5  37691  areacirc  37692  mettrifi  37736  drngoi  37930  eldm4  38248  exanres2  38270  disjecxrn  38360  brcoss2  38408  br1cossres2  38416  eldmcoss2  38435  eldm1cossres2  38437  brcosscnv2  38449  erimeq2  38655  disjlem19  38778  prter3  38860  islshpat  38995  lsatnle  39022  ellkr2  39069  lshpkr  39095  lkr0f2  39139  lduallkr3  39140  lkreqN  39148  cvrval2  39252  isat3  39285  glbconN  39355  glbconNOLD  39356  hlrelat5N  39380  cvrval4N  39393  atlt  39416  1cvrco  39451  pmaple  39740  isline2  39753  isline4N  39756  elpaddn0  39779  elpadd2at2  39786  cdlemkid4  40913  dia0  41031  cdlemm10N  41097  dibglbN  41145  dihmeetlem4preN  41285  dochkrshp3  41367  dvh4dimlem  41422  lcfl5  41475  mapdpglem3  41654  mapdheq  41707  hdmap1eq  41780  hdmapval2lem  41810  hdmapoc  41910  hlhillcs  41937  lcmineqlem18  42019  dvdsexpb  42308  renegadd  42345  resubadd  42352  redivmuld  42418  mulgt0b1d  42445  fsuppssind  42566  fz1eqin  42742  diophin  42745  jm2.19  42966  rmxdiophlem  42988  pw2f1ocnv  43010  wepwsolem  43015  gicabl  43072  idomodle  43164  onsupmaxb  43212  cantnf2  43298  tfsconcatb0  43317  tfsnfin  43325  ntrclsfveq2  44034  ntrclsss  44036  ntrclsk4  44045  extoimad  44137  radcnvrat  44287  bcc0  44313  supxrre3rnmpt  45409  clim2f  45618  clim2f2  45652  liminfreuzlem  45784  liminfltlem  45786  xlimmnflimsup2  45834  xlimpnfliminf2  45843  xlimlimsupleliminf  45845  opprb  47016  funbrafv2b  47144  dfafn5a  47145  leaddsuble  47282  mod2addne  47349  iccpartgtprec  47405  flsqrt  47578  dfeven2  47634  dfodd3  47635  lindslinindimp2lem4  48434  snlindsntor  48444  regt1loggt0  48509  elbigo2  48525  elbigolo1  48530  fldivexpfllog2  48538  nnlog2ge0lt1  48539  blenpw2m1  48552  naryfvalelwrdf  48606  isprsd  48927  resccatlem  49046  functhinclem1  49417  thincciso  49426  thinciso  49443  isinito2lem  49471  fulltermc  49484  prstcprs  49533  oduoppcciso  49539  postc  49542  lmdran  49644  cmdlan  49645