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  4485  issn  4796  disjprg  5103  reuhypd  5374  snelpwg  5402  ordtri3  6368  ordsssuc  6423  iota1  6488  funbrfv2b  6918  dffn5  6919  feqmptdf  6931  unima  6936  dmfco  6957  fneqeql  7018  f1ompt  7083  dff13  7229  fliftcnv  7286  soisores  7302  isotr  7311  isoini  7313  caovord3  7602  releldm2  8022  fimaproj  8114  brtpos  8214  tpostpos  8225  oe1m  8509  oawordri  8514  oalimcl  8524  omlimcl  8542  omabs  8615  iserd  8697  qliftel  8773  qliftfun  8775  qliftf  8778  ecopovsym  8792  pw2f1olem  9045  mapen  9105  findcard3  9229  suppeqfsuppbi  9330  mapfien  9359  supisolem  9425  cantnflem1  9642  wemapwe  9650  rankr1clem  9773  rankr1c  9774  ranklim  9797  r1pwALT  9799  r1pwcl  9800  isfin1-2  10338  isfin1-4  10340  fin71num  10350  axdc3lem2  10404  ltmnq  10925  prlem936  11000  ltsosr  11047  ltasr  11053  xrlenlt  11239  ltxrlt  11244  letri3  11259  ne0gt0  11279  subadd  11424  ltsubadd2  11649  lesubadd2  11651  suble  11656  ltsub23  11658  ltaddpos2  11669  ltsubpos  11670  subge02  11694  ltord2  11707  leord2  11708  ltaddsublt  11805  divmul  11840  divmul3  11842  rec11r  11881  ltdiv1  12047  ltdivmul2  12060  ledivmul2  12062  ltrec  12065  ltdiv2  12069  negfi  12132  negiso  12163  nnle1eq1  12216  avgle1  12422  avgle2  12423  avgle  12424  nn0le0eq0  12470  elz2  12547  znnnlt1  12560  zleltp1  12584  difrp  12991  xrltlen  13106  dfle2  13107  xrletri3  13114  xgepnf  13125  xlemnf  13127  qbtwnre  13159  xltnegi  13176  supxrre  13287  infxrre  13297  elioo5  13364  elfz5  13477  elfzm11  13556  predfz  13614  flbi  13778  flbi2  13779  fldiv4lem1div2uz2  13798  fznnfl  13824  zmodid2  13861  2submod  13897  lt2sq  14098  le2sq  14099  sqlecan  14174  bcval5  14283  pfxsuffeqwrdeq  14663  shftfib  15038  mulre  15087  cnpart  15206  01sqrexlem6  15213  sqrmo  15217  elicc4abs  15286  abs2difabs  15301  cau4  15323  limsupgre  15447  clim2  15470  ello1mpt2  15488  lo1resb  15530  o1resb  15532  climeq  15533  climmpt2  15539  isercoll  15634  caucvgb  15646  fsumabs  15767  isumshft  15805  geomulcvg  15842  absefib  16166  dvdsval3  16226  addmulmodb  16235  dvdsabseq  16283  dvdsflip  16287  dvdsssfz1  16288  mod2eq1n2dvds  16317  ndvdsadd  16380  bitscmp  16408  smupvallem  16453  dvdssq  16537  lcmdvds  16578  ncoprmgcdgt1b  16621  isprm3  16653  isprm5  16677  phiprmpw  16746  prmdiv  16755  pc11  16851  pcz  16852  pockthlem  16876  prmreclem2  16888  prmreclem4  16890  prmreclem6  16892  1arith  16898  vdwapun  16945  rami  16986  ramcl  17000  pwsle  17455  ercpbllem  17511  invsym  17724  funcres2c  17865  latnle  18432  grpinvcnv  18938  subgacs  19093  eqger  19110  ghmqusker  19219  gexdvds2  19515  pgpfi1  19525  pgpfi  19535  lsmass  19599  lssnle  19604  lsmdisj3b  19620  lsmhash  19635  ablsubadd  19739  gsumval3lem2  19836  subgdmdprd  19966  pgpfac1lem2  20007  dvdsr02  20281  issubrg3  20509  isdomn3  20624  drngid2  20661  sdrgunit  20705  sdrgacs  20710  lssacs  20873  prmirred  21384  chrdvds  21436  chrcong  21437  chrnzr  21440  znleval  21464  znleval2  21465  cygznlem3  21479  frlmbas  21664  elfilspd  21712  lindfmm  21736  islindf4  21747  islindf5  21748  psrbaglefi  21835  coe1mul2lem1  22153  mdetunilem9  22507  isneip  22992  neiptopnei  23019  lpdifsn  23030  restopnb  23062  restopn2  23064  restdis  23065  restperf  23071  lmbr2  23146  cncls2  23160  cnprest  23176  cnprest2  23177  iscnrm2  23225  ist0-2  23231  ist1-3  23236  ishaus2  23238  cmpfi  23295  dfconn2  23306  1stccnp  23349  subislly  23368  hausmapdom  23387  tx1cn  23496  tx2cn  23497  txcnmpt  23511  txrest  23518  hauseqlcld  23533  tgqtop  23599  qtopcld  23600  ordthmeolem  23688  trfil2  23774  trfil3  23775  trnei  23779  ufildr  23818  fmfg  23836  rnelfm  23840  fmfnfm  23845  elflim  23858  flimrest  23870  cnflf  23889  cnflf2  23890  ptcmplem2  23940  ghmcnp  24002  tsmssubm  24030  iscfilu  24175  xmetgt0  24246  prdsxmetlem  24256  blcomps  24281  blcom  24282  xblpnfps  24283  xblpnf  24284  blpnf  24285  xmeter  24321  setsxms  24367  imasf1obl  24376  stdbdbl  24405  metrest  24412  metuel2  24453  dscopn  24461  xrtgioo  24695  metdstri  24740  cnmpopc  24822  iihalf2  24828  icopnfhmeo  24841  evth2  24859  lmmbr3  25160  iscau3  25178  metcld  25206  cfilucfil3  25220  srabn  25260  rrxmet  25308  minveclem4  25332  evthicc2  25361  ovolgelb  25381  shft2rab  25409  ovolshftlem1  25410  sca2rab  25413  ovolscalem1  25414  ioombl1lem4  25462  mbfmulc2lem  25548  ismbf3d  25555  mbfsup  25565  mbfinf  25566  i1f1lem  25590  i1fmulclem  25603  mbfi1fseqlem4  25619  itg2seq  25643  ditgneg  25758  limcdif  25777  limcnlp  25779  cnplimc  25788  rolle  25894  mvth  25897  dvne0  25916  lhop1lem  25918  itgsubst  25956  mdegle0  25982  deg1leb  26000  deg1le0  26016  q1peqb  26061  coemulhi  26159  dgrlt  26172  plydivlem3  26203  vieta1lem2  26219  aannenlem1  26236  ulmres  26297  reefiso  26358  pilem3  26363  ellogdm  26548  root1eq1  26665  angpieqvdlem  26738  angpieqvdlem2  26739  quad2  26749  1cubr  26752  quart  26771  rlimcnp  26875  wilthlem2  26979  isppw  27024  dvdsflsumcom  27098  fsumvma  27124  logfac2  27128  chpchtsum  27130  dchrmulcl  27160  dchrresb  27170  bclbnd  27191  bposlem1  27195  bposlem5  27199  gausslemma2dlem0c  27269  lgsquadlem1  27291  m1lgs  27299  2lgsoddprmlem2  27320  dchrisumlem3  27402  dchrisum0lem1  27427  sltval2  27568  noextenddif  27580  sleloe  27666  sletri3  27667  eqscut  27717  elmade2  27780  sltadd1  27899  negsunif  27961  sltsub1  27980  sltsubadd2d  27994  mulsproplem12  28030  sltmul2  28074  sltmul1d  28076  divsmulw  28096  sltdivmul2wd  28103  onsiso  28169  n0subs  28253  n0sleltp1  28256  elzn0s  28286  zs12ge0  28342  tgjustr  28401  trgcgrg  28442  lnrot1  28550  islnopp  28666  ismidb  28705  islmib  28714  axsegconlem6  28849  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem12  28902  ausgrusgrb  29092  nb3grpr2  29310  cplgr2v  29359  umgr2v2enb1  29454  crctcsh  29754  clwwlknonwwlknonb  30035  eupth2lems  30167  nmoreltpnf  30698  isblo2  30712  nmlnogt0  30726  phoeqi  30786  ubthlem2  30800  hire  31023  normgt0  31056  ho01i  31757  ho02i  31758  hoeq1  31759  hoeq2  31760  nmopreltpnf  31798  adjeq  31864  leop  32052  leopmul2i  32064  pjnormssi  32097  pjimai  32105  jplem1  32197  mddmd2  32238  mdslmd1lem1  32254  mdslmd1lem2  32255  superpos  32283  atnssm0  32305  dmdbr5ati  32351  disjunsn  32523  fcoinvbr  32534  ofpreima  32589  funcnv5mpt  32592  suppiniseg  32609  isoun  32625  fpwrelmapffslem  32655  fpwrelmap  32656  iocinioc2  32702  xrdifh  32703  nndiffz1  32709  sgn3da  32759  xdivmul  32845  cntzsnid  33009  cntrval2  33128  isarchi2  33139  erler  33216  elrsp  33343  lsmsnpridl  33369  lsmssass  33373  r1pid2OLD  33574  finexttrb  33660  algextdeglem6  33712  algextdeglem7  33713  smatrcl  33786  rhmpreimacnlem  33874  sqsscirc2  33899  xrmulc1cn  33920  esumfsup  34060  1stmbfm  34251  2ndmbfm  34252  mbfmcnt  34259  eulerpartlems  34351  eulerpartlemd  34357  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsima  34507  ballotlemfrcn0  34521  reprinfz1  34613  reprdifc  34618  bnj1173  34992  vonf1owev  35095  zltp1ne  35097  lfuhgr2  35106  erdszelem7  35184  erdszelem9  35186  iscvm  35246  cvmlift3lem4  35309  rexxfr3dALT  35626  fscgr  36068  seglelin  36104  btwnoutside  36113  lineunray  36135  cldbnd  36314  isfne4  36328  fneval  36340  filnetlem4  36369  nndivsub  36445  bj-gabima  36928  dfgcd3  37312  fvineqsneu  37399  wl-sbhbt  37542  wl-sbcom2d  37549  wl-sbalnae  37550  wl-ax11-lem8  37580  sin2h  37604  cos2h  37605  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  ptrest  37613  poimirlem3  37617  poimirlem4  37618  poimirlem22  37636  poimirlem27  37641  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem  37665  itg2addnclem2  37666  itg2gt0cn  37669  iblabsnclem  37677  ftc1anclem6  37692  areacirclem2  37703  areacirclem5  37706  areacirc  37707  mettrifi  37751  drngoi  37945  eldm4  38263  exanres2  38285  disjecxrn  38375  brcoss2  38423  br1cossres2  38431  eldmcoss2  38450  eldm1cossres2  38452  brcosscnv2  38464  erimeq2  38670  disjlem19  38793  prter3  38875  islshpat  39010  lsatnle  39037  ellkr2  39084  lshpkr  39110  lkr0f2  39154  lduallkr3  39155  lkreqN  39163  cvrval2  39267  isat3  39300  glbconN  39370  glbconNOLD  39371  hlrelat5N  39395  cvrval4N  39408  atlt  39431  1cvrco  39466  pmaple  39755  isline2  39768  isline4N  39771  elpaddn0  39794  elpadd2at2  39801  cdlemkid4  40928  dia0  41046  cdlemm10N  41112  dibglbN  41160  dihmeetlem4preN  41300  dochkrshp3  41382  dvh4dimlem  41437  lcfl5  41490  mapdpglem3  41669  mapdheq  41722  hdmap1eq  41795  hdmapval2lem  41825  hdmapoc  41925  hlhillcs  41952  lcmineqlem18  42034  dvdsexpb  42323  renegadd  42360  resubadd  42367  redivmuld  42433  mulgt0b1d  42460  fsuppssind  42581  fz1eqin  42757  diophin  42760  jm2.19  42982  rmxdiophlem  43004  pw2f1ocnv  43026  wepwsolem  43031  gicabl  43088  idomodle  43180  onsupmaxb  43228  cantnf2  43314  tfsconcatb0  43333  tfsnfin  43341  ntrclsfveq2  44050  ntrclsss  44052  ntrclsk4  44061  extoimad  44153  radcnvrat  44303  bcc0  44329  supxrre3rnmpt  45425  clim2f  45634  clim2f2  45668  liminfreuzlem  45800  liminfltlem  45802  xlimmnflimsup2  45850  xlimpnfliminf2  45859  xlimlimsupleliminf  45861  opprb  47032  funbrafv2b  47160  dfafn5a  47161  leaddsuble  47298  mod2addne  47365  iccpartgtprec  47421  flsqrt  47594  dfeven2  47650  dfodd3  47651  lindslinindimp2lem4  48450  snlindsntor  48460  regt1loggt0  48525  elbigo2  48541  elbigolo1  48546  fldivexpfllog2  48554  nnlog2ge0lt1  48555  blenpw2m1  48568  naryfvalelwrdf  48622  isprsd  48943  resccatlem  49062  functhinclem1  49433  thincciso  49442  thinciso  49459  isinito2lem  49487  fulltermc  49500  prstcprs  49549  oduoppcciso  49555  postc  49558  lmdran  49660  cmdlan  49661