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  708  sb3b  2481  sbcom3  2511  sbal1  2533  sbal2  2534  2reu4lem  4477  issn  4789  disjprg  5095  reuhypd  5365  snelpwg  5392  ordtri3  6354  ordsssuc  6409  iota1  6472  funbrfv2b  6892  dffn5  6893  feqmptdf  6905  unima  6910  dmfco  6931  fneqeql  6993  f1ompt  7058  dff13  7202  fliftcnv  7259  soisores  7275  isotr  7284  isoini  7286  caovord3  7573  releldm2  7989  fimaproj  8079  brtpos  8179  tpostpos  8190  oe1m  8474  oawordri  8479  oalimcl  8489  omlimcl  8507  omabs  8581  iserd  8664  qliftel  8741  qliftfun  8743  qliftf  8746  ecopovsym  8760  pw2f1olem  9013  mapen  9073  findcard3  9187  tfsnfin2  9267  suppeqfsuppbi  9286  mapfien  9315  supisolem  9381  cantnflem1  9602  wemapwe  9610  rankr1clem  9736  rankr1c  9737  ranklim  9760  r1pwALT  9762  r1pwcl  9763  isfin1-2  10299  isfin1-4  10301  fin71num  10311  axdc3lem2  10365  infinfg  10480  ltmnq  10887  prlem936  10962  ltsosr  11009  ltasr  11015  xrlenlt  11201  ltxrlt  11207  letri3  11222  ne0gt0  11242  subadd  11387  ltsubadd2  11612  lesubadd2  11614  suble  11619  ltsub23  11621  ltaddpos2  11632  ltsubpos  11633  subge02  11657  ltord2  11670  leord2  11671  ltaddsublt  11768  divmul  11803  divmul3  11805  rec11r  11844  ltdiv1  12010  ltdivmul2  12023  ledivmul2  12025  ltrec  12028  ltdiv2  12032  negfi  12095  negiso  12126  nnle1eq1  12179  avgle1  12385  avgle2  12386  avgle  12387  nn0le0eq0  12433  elz2  12510  znnnlt1  12522  zleltp1  12546  difrp  12949  xrltlen  13064  dfle2  13065  xrletri3  13072  xgepnf  13084  xlemnf  13086  qbtwnre  13118  xltnegi  13135  supxrre  13246  infxrre  13256  elioo5  13323  elfz5  13436  elfzm11  13515  predfz  13573  flbi  13740  flbi2  13741  fldiv4lem1div2uz2  13760  fznnfl  13786  zmodid2  13823  2submod  13859  lt2sq  14060  le2sq  14061  sqlecan  14136  bcval5  14245  pfxsuffeqwrdeq  14625  shftfib  14999  mulre  15048  cnpart  15167  01sqrexlem6  15174  sqrmo  15178  elicc4abs  15247  abs2difabs  15262  cau4  15284  limsupgre  15408  clim2  15431  ello1mpt2  15449  lo1resb  15491  o1resb  15493  climeq  15494  climmpt2  15500  isercoll  15595  caucvgb  15607  fsumabs  15728  isumshft  15766  geomulcvg  15803  absefib  16127  dvdsval3  16187  addmulmodb  16196  dvdsabseq  16244  dvdsflip  16248  dvdsssfz1  16249  mod2eq1n2dvds  16278  ndvdsadd  16341  bitscmp  16369  smupvallem  16414  dvdssq  16498  lcmdvds  16539  ncoprmgcdgt1b  16582  isprm3  16614  isprm5  16638  phiprmpw  16707  prmdiv  16716  pc11  16812  pcz  16813  pockthlem  16837  prmreclem2  16849  prmreclem4  16851  prmreclem6  16853  1arith  16859  vdwapun  16906  rami  16947  ramcl  16961  pwsle  17417  ercpbllem  17473  invsym  17690  funcres2c  17831  latnle  18400  grpinvcnv  18940  subgacs  19094  eqger  19111  ghmqusker  19220  gexdvds2  19518  pgpfi1  19528  pgpfi  19538  lsmass  19602  lssnle  19607  lsmdisj3b  19623  lsmhash  19638  ablsubadd  19742  gsumval3lem2  19839  subgdmdprd  19969  pgpfac1lem2  20010  dvdsr02  20312  issubrg3  20537  isdomn3  20652  drngid2  20689  sdrgunit  20733  sdrgacs  20738  lssacs  20922  prmirred  21433  chrdvds  21485  chrcong  21486  chrnzr  21489  znleval  21513  znleval2  21514  cygznlem3  21528  frlmbas  21714  elfilspd  21762  lindfmm  21786  islindf4  21797  islindf5  21798  psrbaglefi  21886  coe1mul2lem1  22213  mdetunilem9  22568  isneip  23053  neiptopnei  23080  lpdifsn  23091  restopnb  23123  restopn2  23125  restdis  23126  restperf  23132  lmbr2  23207  cncls2  23221  cnprest  23237  cnprest2  23238  iscnrm2  23286  ist0-2  23292  ist1-3  23297  ishaus2  23299  cmpfi  23356  dfconn2  23367  1stccnp  23410  subislly  23429  hausmapdom  23448  tx1cn  23557  tx2cn  23558  txcnmpt  23572  txrest  23579  hauseqlcld  23594  tgqtop  23660  qtopcld  23661  ordthmeolem  23749  trfil2  23835  trfil3  23836  trnei  23840  ufildr  23879  fmfg  23897  rnelfm  23901  fmfnfm  23906  elflim  23919  flimrest  23931  cnflf  23950  cnflf2  23951  ptcmplem2  24001  ghmcnp  24063  tsmssubm  24091  iscfilu  24235  xmetgt0  24306  prdsxmetlem  24316  blcomps  24341  blcom  24342  xblpnfps  24343  xblpnf  24344  blpnf  24345  xmeter  24381  setsxms  24427  imasf1obl  24436  stdbdbl  24465  metrest  24472  metuel2  24513  dscopn  24521  xrtgioo  24755  metdstri  24800  cnmpopc  24882  iihalf2  24888  icopnfhmeo  24901  evth2  24919  lmmbr3  25220  iscau3  25238  metcld  25266  cfilucfil3  25280  srabn  25320  rrxmet  25368  minveclem4  25392  evthicc2  25421  ovolgelb  25441  shft2rab  25469  ovolshftlem1  25470  sca2rab  25473  ovolscalem1  25474  ioombl1lem4  25522  mbfmulc2lem  25608  ismbf3d  25615  mbfsup  25625  mbfinf  25626  i1f1lem  25650  i1fmulclem  25663  mbfi1fseqlem4  25679  itg2seq  25703  ditgneg  25818  limcdif  25837  limcnlp  25839  cnplimc  25848  rolle  25954  mvth  25957  dvne0  25976  lhop1lem  25978  itgsubst  26016  mdegle0  26042  deg1leb  26060  deg1le0  26076  q1peqb  26121  coemulhi  26219  dgrlt  26232  plydivlem3  26263  vieta1lem2  26279  aannenlem1  26296  ulmres  26357  reefiso  26418  pilem3  26423  ellogdm  26608  root1eq1  26725  angpieqvdlem  26798  angpieqvdlem2  26799  quad2  26809  1cubr  26812  quart  26831  rlimcnp  26935  wilthlem2  27039  isppw  27084  dvdsflsumcom  27158  fsumvma  27184  logfac2  27188  chpchtsum  27190  dchrmulcl  27220  dchrresb  27230  bclbnd  27251  bposlem1  27255  bposlem5  27259  gausslemma2dlem0c  27329  lgsquadlem1  27351  m1lgs  27359  2lgsoddprmlem2  27380  dchrisumlem3  27462  dchrisum0lem1  27487  sltval2  27628  noextenddif  27640  sleloe  27726  sletri3  27727  eqscut  27783  elmade2  27850  sltadd1  27974  negsunif  28037  sltsub1  28058  sltsubadd2d  28072  mulsproplem12  28109  sltmul2  28153  sltmul1d  28155  divsmulw  28175  sltdivmul2wd  28182  onsiso  28252  n0subs  28342  n0sleltp1  28345  elzn0s  28377  avgslt1d  28432  avgslt2d  28433  bdaypw2n0sbndlem  28442  bdayfinbndlem1  28446  zs12ge0  28462  dfzs122  28467  elreno2  28474  tgjustr  28529  trgcgrg  28570  lnrot1  28678  islnopp  28794  ismidb  28833  islmib  28842  axsegconlem6  28978  axeuclidlem  29018  axcontlem2  29021  axcontlem4  29023  axcontlem12  29031  ausgrusgrb  29221  nb3grpr2  29439  cplgr2v  29488  umgr2v2enb1  29583  crctcsh  29880  clwwlknonwwlknonb  30164  eupth2lems  30296  nmoreltpnf  30827  isblo2  30841  nmlnogt0  30855  phoeqi  30915  ubthlem2  30929  hire  31152  normgt0  31185  ho01i  31886  ho02i  31887  hoeq1  31888  hoeq2  31889  nmopreltpnf  31927  adjeq  31993  leop  32181  leopmul2i  32193  pjnormssi  32226  pjimai  32234  jplem1  32326  mddmd2  32367  mdslmd1lem1  32383  mdslmd1lem2  32384  superpos  32412  atnssm0  32434  dmdbr5ati  32480  disjunsn  32651  fcoinvbr  32662  ofpreima  32725  funcnv5mpt  32727  suppiniseg  32746  isoun  32762  fpwrelmapffslem  32792  fpwrelmap  32793  iocinioc2  32840  xrdifh  32841  nndiffz1  32847  sgn3da  32896  xdivmul  32987  cntzsnid  33143  cntrval2  33234  isarchi2  33248  erler  33328  elrsp  33434  lsmsnpridl  33460  lsmssass  33464  r1pid2OLD  33671  esplyind  33712  finexttrb  33803  algextdeglem6  33860  algextdeglem7  33861  smatrcl  33934  rhmpreimacnlem  34022  sqsscirc2  34047  xrmulc1cn  34068  esumfsup  34208  1stmbfm  34398  2ndmbfm  34399  mbfmcnt  34406  eulerpartlems  34498  eulerpartlemd  34504  ballotlemfc0  34631  ballotlemfcc  34632  ballotlemsima  34654  ballotlemfrcn0  34668  reprinfz1  34760  reprdifc  34765  bnj1173  35139  fineqvnttrclse  35261  vonf1owev  35283  zltp1ne  35285  lfuhgr2  35294  erdszelem7  35372  erdszelem9  35374  iscvm  35434  cvmlift3lem4  35497  rexxfr3dALT  35814  fscgr  36255  seglelin  36291  btwnoutside  36300  lineunray  36322  cldbnd  36501  isfne4  36515  fneval  36527  filnetlem4  36556  nndivsub  36632  bj-gabima  37116  dfgcd3  37500  fvineqsneu  37587  wl-sbhbt  37730  wl-sbcom2d  37737  wl-sbalnae  37738  sin2h  37782  cos2h  37783  matunitlindflem1  37788  matunitlindflem2  37789  matunitlindf  37790  ptrest  37791  poimirlem3  37795  poimirlem4  37796  poimirlem22  37814  poimirlem27  37819  mblfinlem3  37831  mblfinlem4  37832  ismblfin  37833  itg2addnclem  37843  itg2addnclem2  37844  itg2gt0cn  37847  iblabsnclem  37855  ftc1anclem6  37870  areacirclem2  37881  areacirclem5  37884  areacirc  37885  mettrifi  37929  drngoi  38123  eldm4  38453  exanres2  38475  disjecxrn  38584  exeupre  38663  brcoss2  38694  br1cossres2  38702  eldmcoss2  38721  eldm1cossres2  38723  brcosscnv2  38735  erimeq2  38935  disjqmap  38999  disjlem19  39076  prter3  39179  islshpat  39314  lsatnle  39341  ellkr2  39388  lshpkr  39414  lkr0f2  39458  lduallkr3  39459  lkreqN  39467  cvrval2  39571  isat3  39604  glbconN  39674  hlrelat5N  39698  cvrval4N  39711  atlt  39734  1cvrco  39769  pmaple  40058  isline2  40071  isline4N  40074  elpaddn0  40097  elpadd2at2  40104  cdlemkid4  41231  dia0  41349  cdlemm10N  41415  dibglbN  41463  dihmeetlem4preN  41603  dochkrshp3  41685  dvh4dimlem  41740  lcfl5  41793  mapdpglem3  41972  mapdheq  42025  hdmap1eq  42098  hdmapval2lem  42128  hdmapoc  42228  hlhillcs  42255  lcmineqlem18  42337  dvdsexpb  42626  renegadd  42663  resubadd  42670  redivmuld  42736  mulgt0b1d  42763  fsuppssind  42872  fz1eqin  43047  diophin  43050  jm2.19  43271  rmxdiophlem  43293  pw2f1ocnv  43315  wepwsolem  43320  gicabl  43377  idomodle  43469  onsupmaxb  43517  cantnf2  43603  tfsconcatb0  43622  tfsnfin  43630  ntrclsfveq2  44338  ntrclsss  44340  ntrclsk4  44349  extoimad  44441  radcnvrat  44591  bcc0  44617  supxrre3rnmpt  45709  clim2f  45916  clim2f2  45950  liminfreuzlem  46082  liminfltlem  46084  xlimmnflimsup2  46132  xlimpnfliminf2  46141  xlimlimsupleliminf  46143  opprb  47313  funbrafv2b  47441  dfafn5a  47442  leaddsuble  47579  mod2addne  47646  iccpartgtprec  47702  flsqrt  47875  dfeven2  47931  dfodd3  47932  lindslinindimp2lem4  48743  snlindsntor  48753  regt1loggt0  48818  elbigo2  48834  elbigolo1  48839  fldivexpfllog2  48847  nnlog2ge0lt1  48848  blenpw2m1  48861  naryfvalelwrdf  48915  isprsd  49236  resccatlem  49354  functhinclem1  49725  thincciso  49734  thinciso  49751  isinito2lem  49779  fulltermc  49792  prstcprs  49841  oduoppcciso  49847  postc  49850  lmdran  49952  cmdlan  49953