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  2475  sbcom3  2505  sbal1  2527  sbal2  2528  2reu4lem  4470  issn  4782  disjprg  5085  reuhypd  5355  snelpwg  5382  ordtri3  6338  ordsssuc  6393  iota1  6456  funbrfv2b  6874  dffn5  6875  feqmptdf  6887  unima  6892  dmfco  6913  fneqeql  6974  f1ompt  7039  dff13  7183  fliftcnv  7240  soisores  7256  isotr  7265  isoini  7267  caovord3  7554  releldm2  7970  fimaproj  8060  brtpos  8160  tpostpos  8171  oe1m  8455  oawordri  8460  oalimcl  8470  omlimcl  8488  omabs  8561  iserd  8643  qliftel  8719  qliftfun  8721  qliftf  8724  ecopovsym  8738  pw2f1olem  8989  mapen  9049  findcard3  9162  suppeqfsuppbi  9258  mapfien  9287  supisolem  9353  cantnflem1  9574  wemapwe  9582  rankr1clem  9705  rankr1c  9706  ranklim  9729  r1pwALT  9731  r1pwcl  9732  isfin1-2  10268  isfin1-4  10270  fin71num  10280  axdc3lem2  10334  ltmnq  10855  prlem936  10930  ltsosr  10977  ltasr  10983  xrlenlt  11169  ltxrlt  11175  letri3  11190  ne0gt0  11210  subadd  11355  ltsubadd2  11580  lesubadd2  11582  suble  11587  ltsub23  11589  ltaddpos2  11600  ltsubpos  11601  subge02  11625  ltord2  11638  leord2  11639  ltaddsublt  11736  divmul  11771  divmul3  11773  rec11r  11812  ltdiv1  11978  ltdivmul2  11991  ledivmul2  11993  ltrec  11996  ltdiv2  12000  negfi  12063  negiso  12094  nnle1eq1  12147  avgle1  12353  avgle2  12354  avgle  12355  nn0le0eq0  12401  elz2  12478  znnnlt1  12491  zleltp1  12515  difrp  12922  xrltlen  13037  dfle2  13038  xrletri3  13045  xgepnf  13056  xlemnf  13058  qbtwnre  13090  xltnegi  13107  supxrre  13218  infxrre  13228  elioo5  13295  elfz5  13408  elfzm11  13487  predfz  13545  flbi  13712  flbi2  13713  fldiv4lem1div2uz2  13732  fznnfl  13758  zmodid2  13795  2submod  13831  lt2sq  14032  le2sq  14033  sqlecan  14108  bcval5  14217  pfxsuffeqwrdeq  14597  shftfib  14971  mulre  15020  cnpart  15139  01sqrexlem6  15146  sqrmo  15150  elicc4abs  15219  abs2difabs  15234  cau4  15256  limsupgre  15380  clim2  15403  ello1mpt2  15421  lo1resb  15463  o1resb  15465  climeq  15466  climmpt2  15472  isercoll  15567  caucvgb  15579  fsumabs  15700  isumshft  15738  geomulcvg  15775  absefib  16099  dvdsval3  16159  addmulmodb  16168  dvdsabseq  16216  dvdsflip  16220  dvdsssfz1  16221  mod2eq1n2dvds  16250  ndvdsadd  16313  bitscmp  16341  smupvallem  16386  dvdssq  16470  lcmdvds  16511  ncoprmgcdgt1b  16554  isprm3  16586  isprm5  16610  phiprmpw  16679  prmdiv  16688  pc11  16784  pcz  16785  pockthlem  16809  prmreclem2  16821  prmreclem4  16823  prmreclem6  16825  1arith  16831  vdwapun  16878  rami  16919  ramcl  16933  pwsle  17388  ercpbllem  17444  invsym  17661  funcres2c  17802  latnle  18371  grpinvcnv  18911  subgacs  19066  eqger  19083  ghmqusker  19192  gexdvds2  19490  pgpfi1  19500  pgpfi  19510  lsmass  19574  lssnle  19579  lsmdisj3b  19595  lsmhash  19610  ablsubadd  19714  gsumval3lem2  19811  subgdmdprd  19941  pgpfac1lem2  19982  dvdsr02  20283  issubrg3  20508  isdomn3  20623  drngid2  20660  sdrgunit  20704  sdrgacs  20709  lssacs  20893  prmirred  21404  chrdvds  21456  chrcong  21457  chrnzr  21460  znleval  21484  znleval2  21485  cygznlem3  21499  frlmbas  21685  elfilspd  21733  lindfmm  21757  islindf4  21768  islindf5  21769  psrbaglefi  21856  coe1mul2lem1  22174  mdetunilem9  22528  isneip  23013  neiptopnei  23040  lpdifsn  23051  restopnb  23083  restopn2  23085  restdis  23086  restperf  23092  lmbr2  23167  cncls2  23181  cnprest  23197  cnprest2  23198  iscnrm2  23246  ist0-2  23252  ist1-3  23257  ishaus2  23259  cmpfi  23316  dfconn2  23327  1stccnp  23370  subislly  23389  hausmapdom  23408  tx1cn  23517  tx2cn  23518  txcnmpt  23532  txrest  23539  hauseqlcld  23554  tgqtop  23620  qtopcld  23621  ordthmeolem  23709  trfil2  23795  trfil3  23796  trnei  23800  ufildr  23839  fmfg  23857  rnelfm  23861  fmfnfm  23866  elflim  23879  flimrest  23891  cnflf  23910  cnflf2  23911  ptcmplem2  23961  ghmcnp  24023  tsmssubm  24051  iscfilu  24195  xmetgt0  24266  prdsxmetlem  24276  blcomps  24301  blcom  24302  xblpnfps  24303  xblpnf  24304  blpnf  24305  xmeter  24341  setsxms  24387  imasf1obl  24396  stdbdbl  24425  metrest  24432  metuel2  24473  dscopn  24481  xrtgioo  24715  metdstri  24760  cnmpopc  24842  iihalf2  24848  icopnfhmeo  24861  evth2  24879  lmmbr3  25180  iscau3  25198  metcld  25226  cfilucfil3  25240  srabn  25280  rrxmet  25328  minveclem4  25352  evthicc2  25381  ovolgelb  25401  shft2rab  25429  ovolshftlem1  25430  sca2rab  25433  ovolscalem1  25434  ioombl1lem4  25482  mbfmulc2lem  25568  ismbf3d  25575  mbfsup  25585  mbfinf  25586  i1f1lem  25610  i1fmulclem  25623  mbfi1fseqlem4  25639  itg2seq  25663  ditgneg  25778  limcdif  25797  limcnlp  25799  cnplimc  25808  rolle  25914  mvth  25917  dvne0  25936  lhop1lem  25938  itgsubst  25976  mdegle0  26002  deg1leb  26020  deg1le0  26036  q1peqb  26081  coemulhi  26179  dgrlt  26192  plydivlem3  26223  vieta1lem2  26239  aannenlem1  26256  ulmres  26317  reefiso  26378  pilem3  26383  ellogdm  26568  root1eq1  26685  angpieqvdlem  26758  angpieqvdlem2  26759  quad2  26769  1cubr  26772  quart  26791  rlimcnp  26895  wilthlem2  26999  isppw  27044  dvdsflsumcom  27118  fsumvma  27144  logfac2  27148  chpchtsum  27150  dchrmulcl  27180  dchrresb  27190  bclbnd  27211  bposlem1  27215  bposlem5  27219  gausslemma2dlem0c  27289  lgsquadlem1  27311  m1lgs  27319  2lgsoddprmlem2  27340  dchrisumlem3  27422  dchrisum0lem1  27447  sltval2  27588  noextenddif  27600  sleloe  27686  sletri3  27687  eqscut  27739  elmade2  27806  sltadd1  27928  negsunif  27990  sltsub1  28009  sltsubadd2d  28023  mulsproplem12  28059  sltmul2  28103  sltmul1d  28105  divsmulw  28125  sltdivmul2wd  28132  onsiso  28198  n0subs  28282  n0sleltp1  28285  elzn0s  28315  avgslt1d  28369  avgslt2d  28370  zs12ge0  28386  tgjustr  28445  trgcgrg  28486  lnrot1  28594  islnopp  28710  ismidb  28749  islmib  28758  axsegconlem6  28893  axeuclidlem  28933  axcontlem2  28936  axcontlem4  28938  axcontlem12  28946  ausgrusgrb  29136  nb3grpr2  29354  cplgr2v  29403  umgr2v2enb1  29498  crctcsh  29795  clwwlknonwwlknonb  30076  eupth2lems  30208  nmoreltpnf  30739  isblo2  30753  nmlnogt0  30767  phoeqi  30827  ubthlem2  30841  hire  31064  normgt0  31097  ho01i  31798  ho02i  31799  hoeq1  31800  hoeq2  31801  nmopreltpnf  31839  adjeq  31905  leop  32093  leopmul2i  32105  pjnormssi  32138  pjimai  32146  jplem1  32238  mddmd2  32279  mdslmd1lem1  32295  mdslmd1lem2  32296  superpos  32324  atnssm0  32346  dmdbr5ati  32392  disjunsn  32564  fcoinvbr  32575  ofpreima  32637  funcnv5mpt  32640  suppiniseg  32657  isoun  32673  fpwrelmapffslem  32705  fpwrelmap  32706  iocinioc2  32752  xrdifh  32753  nndiffz1  32759  sgn3da  32807  xdivmul  32895  cntzsnid  33039  cntrval2  33130  isarchi2  33144  erler  33222  elrsp  33327  lsmsnpridl  33353  lsmssass  33357  r1pid2OLD  33559  finexttrb  33668  algextdeglem6  33725  algextdeglem7  33726  smatrcl  33799  rhmpreimacnlem  33887  sqsscirc2  33912  xrmulc1cn  33933  esumfsup  34073  1stmbfm  34263  2ndmbfm  34264  mbfmcnt  34271  eulerpartlems  34363  eulerpartlemd  34369  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemsima  34519  ballotlemfrcn0  34533  reprinfz1  34625  reprdifc  34630  bnj1173  35004  fineqvnttrclse  35112  vonf1owev  35120  zltp1ne  35122  lfuhgr2  35131  erdszelem7  35209  erdszelem9  35211  iscvm  35271  cvmlift3lem4  35334  rexxfr3dALT  35651  fscgr  36093  seglelin  36129  btwnoutside  36138  lineunray  36160  cldbnd  36339  isfne4  36353  fneval  36365  filnetlem4  36394  nndivsub  36470  bj-gabima  36953  dfgcd3  37337  fvineqsneu  37424  wl-sbhbt  37567  wl-sbcom2d  37574  wl-sbalnae  37575  wl-ax11-lem8  37605  sin2h  37629  cos2h  37630  matunitlindflem1  37635  matunitlindflem2  37636  matunitlindf  37637  ptrest  37638  poimirlem3  37642  poimirlem4  37643  poimirlem22  37661  poimirlem27  37666  mblfinlem3  37678  mblfinlem4  37679  ismblfin  37680  itg2addnclem  37690  itg2addnclem2  37691  itg2gt0cn  37694  iblabsnclem  37702  ftc1anclem6  37717  areacirclem2  37728  areacirclem5  37731  areacirc  37732  mettrifi  37776  drngoi  37970  eldm4  38288  exanres2  38310  disjecxrn  38400  brcoss2  38448  br1cossres2  38456  eldmcoss2  38475  eldm1cossres2  38477  brcosscnv2  38489  erimeq2  38695  disjlem19  38818  prter3  38900  islshpat  39035  lsatnle  39062  ellkr2  39109  lshpkr  39135  lkr0f2  39179  lduallkr3  39180  lkreqN  39188  cvrval2  39292  isat3  39325  glbconN  39395  hlrelat5N  39419  cvrval4N  39432  atlt  39455  1cvrco  39490  pmaple  39779  isline2  39792  isline4N  39795  elpaddn0  39818  elpadd2at2  39825  cdlemkid4  40952  dia0  41070  cdlemm10N  41136  dibglbN  41184  dihmeetlem4preN  41324  dochkrshp3  41406  dvh4dimlem  41461  lcfl5  41514  mapdpglem3  41693  mapdheq  41746  hdmap1eq  41819  hdmapval2lem  41849  hdmapoc  41949  hlhillcs  41976  lcmineqlem18  42058  dvdsexpb  42347  renegadd  42384  resubadd  42391  redivmuld  42457  mulgt0b1d  42484  fsuppssind  42605  fz1eqin  42781  diophin  42784  jm2.19  43005  rmxdiophlem  43027  pw2f1ocnv  43049  wepwsolem  43054  gicabl  43111  idomodle  43203  onsupmaxb  43251  cantnf2  43337  tfsconcatb0  43356  tfsnfin  43364  ntrclsfveq2  44073  ntrclsss  44075  ntrclsk4  44084  extoimad  44176  radcnvrat  44326  bcc0  44352  supxrre3rnmpt  45446  clim2f  45653  clim2f2  45687  liminfreuzlem  45819  liminfltlem  45821  xlimmnflimsup2  45869  xlimpnfliminf2  45878  xlimlimsupleliminf  45880  opprb  47041  funbrafv2b  47169  dfafn5a  47170  leaddsuble  47307  mod2addne  47374  iccpartgtprec  47430  flsqrt  47603  dfeven2  47659  dfodd3  47660  lindslinindimp2lem4  48472  snlindsntor  48482  regt1loggt0  48547  elbigo2  48563  elbigolo1  48568  fldivexpfllog2  48576  nnlog2ge0lt1  48577  blenpw2m1  48590  naryfvalelwrdf  48644  isprsd  48965  resccatlem  49084  functhinclem1  49455  thincciso  49464  thinciso  49481  isinito2lem  49509  fulltermc  49522  prstcprs  49571  oduoppcciso  49577  postc  49580  lmdran  49682  cmdlan  49683