Theorem bitr4d 285

Description: Deduction form of bitr4i 281. (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 226	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr2d  310  3bitr2rd  311  3bitr4d  314  3bitr4rd  315  bianabs  551  mpbirand  720  sb3b  2505  sbcom3  2535  sbal1  2557  sbal2  2558  2reu4lem  4478  issn  4791  disjprg  5098  reuhypd  5380  snelpwg  5410  ordtri3  6388  ordsssuc  6443  iota1  6506  funbrfv2b  6930  dffn5  6931  feqmptdf  6943  unima  6948  dmfco  6969  fneqeql  7033  f1ompt  7099  dff13  7246  fliftcnv  7307  soisores  7323  isotr  7332  isoini  7334  caovord3  7622  releldm2  8037  fimaproj  8130  brtpos  8230  tpostpos  8241  oe1m  8531  oawordri  8536  oalimcl  8546  omlimcl  8564  omabs  8638  iserd  8722  qliftel  8799  qliftfun  8801  qliftf  8804  ecopovsym  8818  pw2f1olem  9078  mapen  9138  findcard3  9252  tfsnfin2  9330  suppeqfsuppbi  9349  mapfien  9378  supisolem  9444  cantnflem1  9668  wemapwe  9676  rankr1clem  9802  rankr1c  9803  ranklim  9831  r1pwALT  9833  r1pwcl  9834  isfin1-2  10434  isfin1-4  10436  fin71num  10446  axdc3lem2  10500  infinfg  10621  ltmnq  11028  prlem936  11103  ltsosr  11150  ltasr  11156  xrlenlt  11345  ltxrlt  11351  letri3  11366  ne0gt0  11386  subadd  11531  ltsubadd2  11756  lesubadd2  11758  suble  11763  ltsub23  11765  ltaddpos2  11776  ltsubpos  11777  subge02  11801  ltord2  11814  leord2  11815  ltaddsublt  11912  divmul  11946  divmul3  11948  rec11r  11985  ltdiv1  12150  ltdivmul2  12163  ledivmul2  12165  ltrec  12168  ltdiv2  12172  negfi  12235  negiso  12266  nnle1eq1  12337  avgle1  12555  avgle2  12556  avgle  12557  nn0le0eq0  12603  elz2  12680  znnnlt1  12692  zleltp1  12716  difrp  13129  xrltlen  13244  dfle2  13245  xrletri3  13252  xgepnf  13264  xlemnf  13266  qbtwnre  13298  xltnegi  13315  supxrre  13426  infxrre  13436  elioo5  13503  elfz5  13617  elfzm11  13697  predfz  13755  flbi  13924  flbi2  13925  fldiv4lem1div2uz2  13944  fznnfl  13970  zmodid2  14007  2submod  14043  lt2sq  14244  le2sq  14245  sqlecan  14320  bcval5  14429  pfxsuffeqwrdeq  14814  shftfib  15192  sgn3da  15221  mulre  15255  cnpart  15374  01sqrexlem6  15381  sqrmo  15385  elicc4abs  15454  abs2difabs  15469  cau4  15491  limsupgre  15615  clim2  15638  ello1mpt2  15656  lo1resb  15698  o1resb  15700  climeq  15701  climmpt2  15707  isercoll  15802  caucvgb  15814  fsumabs  15935  isumshft  15975  geomulcvg  16012  absefib  16333  dvdsval3  16393  addmulmodb  16402  dvdsabseq  16450  dvdsflip  16454  dvdsssfz1  16455  mod2eq1n2dvds  16484  ndvdsadd  16547  bitscmp  16575  smupvallem  16620  dvdssq  16704  lcmdvds  16745  ncoprmgcdgt1b  16788  isprm3  16820  isprm5  16845  phiprmpw  16914  prmdiv  16923  pc11  17019  pcz  17020  pockthlem  17044  prmreclem2  17056  prmreclem4  17058  prmreclem6  17060  1arith  17066  vdwapun  17113  rami  17154  ramcl  17168  pwsle  17625  ercpbllem  17681  invsym  17898  funcres2c  18039  latnle  18608  grpinvcnv  19178  subgacs  19332  eqger  19351  ghmqusker  19462  gexdvds2  19760  pgpfi1  19770  pgpfi  19780  lsmass  19844  lssnle  19849  lsmdisj3b  19865  lsmhash  19880  ablsubadd  19984  gsumval3lem2  20081  subgdmdprd  20211  pgpfac1lem2  20252  dvdsr02  20563  issubrg3  20813  isdomn3  20927  drngid2  20971  sdrgunit  21014  sdrgacs  21019  lssacs  21203  prmirred  21741  chrdvds  21793  chrcong  21794  chrnzr  21797  znleval  21821  znleval2  21822  cygznlem3  21836  frlmbas  22022  elfilspd  22070  lindfmm  22094  islindf4  22105  islindf5  22106  psrbaglefi  22195  coe1mul2lem1  22547  mdetunilem9  22896  matunitlindflem1  22955  matunitlindflem2  22956  matunitlindf  22957  isneip  23384  neiptopnei  23411  lpdifsn  23422  restopnb  23454  restopn2  23456  restdis  23457  restperf  23463  lmbr2  23538  cncls2  23552  cnprest  23568  cnprest2  23569  iscnrm2  23617  ist0-2  23623  ist1-3  23628  ishaus2  23630  cmpfi  23687  dfconn2  23698  1stccnp  23742  subislly  23761  hausmapdom  23780  tx1cn  23889  tx2cn  23890  txcnmpt  23904  txrest  23911  hauseqlcld  23926  tgqtop  23992  qtopcld  23993  ordthmeolem  24081  trfil2  24167  trfil3  24168  trnei  24172  ufildr  24211  fmfg  24229  rnelfm  24233  fmfnfm  24238  elflim  24251  flimrest  24263  cnflf  24282  cnflf2  24283  ptcmplem2  24333  ghmcnp  24395  tsmssubm  24423  iscfilu  24567  xmetgt0  24638  prdsxmetlem  24648  blcomps  24673  blcom  24674  xblpnfps  24675  xblpnf  24676  blpnf  24677  xmeter  24713  setsxms  24759  imasf1obl  24768  stdbdbl  24797  metrest  24804  metuel2  24845  dscopn  24853  xrtgioo  25087  metdstri  25132  cnmpopc  25210  iihalf2  25215  icopnfhmeo  25225  evth2  25242  lmmbr3  25542  iscau3  25560  metcld  25588  cfilucfil3  25602  srabn  25642  rrxmet  25690  minveclem4  25714  evthicc2  25742  ovolgelb  25762  shft2rab  25790  ovolshftlem1  25791  sca2rab  25794  ovolscalem1  25795  ioombl1lem4  25843  mbfmulc2lem  25929  ismbf3d  25936  mbfsup  25946  mbfinf  25947  i1f1lem  25971  i1fmulclem  25984  mbfi1fseqlem4  26000  itg2seq  26024  ditgneg  26138  limcdif  26157  limcnlp  26159  cnplimc  26168  rolle  26271  mvth  26273  dvne0  26292  lhop1lem  26294  itgsubst  26330  mdegle0  26356  deg1leb  26374  deg1le0  26390  q1peqb  26435  coemulhi  26534  dgrlt  26546  plydivlem3  26579  vieta1lem2  26597  aannenlem1  26618  ulmres  26678  reefiso  26738  pilem3  26743  ellogdm  26930  root1eq1  27046  angpieqvdlem  27119  angpieqvdlem2  27120  quad2  27130  1cubr  27133  quart  27152  rlimcnp  27256  wilthlem2  27359  isppw  27404  dvdsflsumcom  27478  fsumvma  27503  logfac2  27507  chpchtsum  27509  dchrmulcl  27539  dchrresb  27549  bclbnd  27570  bposlem1  27574  bposlem5  27578  gausslemma2dlem0c  27648  lgsquadlem1  27670  m1lgs  27678  2lgsoddprmlem2  27699  dchrisumlem3  27781  dchrisum0lem1  27806  ltsval2  27946  noextenddif  27958  lesloe  28044  lestri3  28045  eqcuts  28104  elmade2  28177  ltadds1  28311  negsunif  28374  ltsubs1  28395  ltsubadds2d  28409  mulsproplem12  28446  ltmuls2  28490  ltmuls1d  28492  divmulsw  28512  ltdivmuls2wd  28519  oniso  28590  n0subs  28682  n0lesltp1  28685  elzn0s  28717  avglts1d  28772  avglts2d  28773  bdaypw2n0bndlem  28782  z12sge0  28802  dfz12s2  28807  elreno2  28814  tgjustr  28869  trgcgrg  28911  lnrot1  29024  islnopp  29148  elplng  29191  plngcplem  29196  ismidb  29216  islmib  29225  axsegconlem6  29433  axeuclidlem  29473  axcontlem2  29476  axcontlem4  29478  axcontlem12  29486  lfuhgr2  29660  ausgrusgrb  29679  nb3grpr2  29897  cplgr2v  29946  umgr2v2enb1  30040  crctcsh  30346  clwwlknonwwlknonb  30630  eupth2lems  30772  nmoreltpnf  31304  isblo2  31318  nmlnogt0  31332  phoeqi  31392  ubthlem2  31406  hire  31629  normgt0  31662  ho01i  32363  ho02i  32364  hoeq1  32365  hoeq2  32366  nmopreltpnf  32404  adjeq  32470  leop  32658  leopmul2i  32670  pjnormssi  32703  pjimai  32711  jplem1  32803  mddmd2  32844  mdslmd1lem1  32860  mdslmd1lem2  32861  superpos  32889  atnssm0  32911  dmdbr5ati  32957  disjunsn  33121  fcoinvbr  33132  ofpreima  33192  funcnv5mpt  33194  suppiniseg  33212  isoun  33228  fpwrelmapffslem  33257  fpwrelmap  33258  iocinioc2  33304  xrdifh  33305  nndiffz1  33311  xdivmul  33424  cntzsnid  33574  cntrval2  33665  isarchi2  33679  isunitc  33735  erler  33759  rlocisunit  33770  elrsp  33860  lsmsnpridl  33884  lsmssass  33886  esplyind  34140  finexttrb  34230  algextdeglem6  34287  algextdeglem7  34288  smatrcl  34361  rhmpreimacnlem  34449  sqsscirc2  34474  xrmulc1cn  34495  esumfsup  34635  1stmbfm  34826  2ndmbfm  34827  mbfmcnt  34834  eulerpartlems  34926  eulerpartlemd  34932  ballotlemfc0  35059  ballotlemfcc  35060  ballotlemsima  35082  ballotlemfrcn0  35096  reprinfz1  35185  reprdifc  35190  bnj1173  35566  fineqvnttrclse  35717  kardcard2  35759  vonf1wev  35812  vonf1owevOLD  35814  zltp1ne  35821  erdszelem7  35883  erdszelem9  35885  iscvm  35945  cvmlift3lem4  36008  rexxfr3dALT  36325  fscgr  36767  seglelin  36803  btwnoutside  36812  lineunray  36834  cldbnd  37036  isfne4  37050  fneval  37062  filnetlem4  37091  nndivsub  37167  bj-gabima  37775  dfgcd3  38165  fvineqsneu  38254  wl-sbhbt  38406  wl-sbcom2d  38413  wl-sbalnae  38414  sin2h  38453  cos2h  38454  ptrest  38457  poimirlem3  38461  poimirlem4  38462  poimirlem22  38480  poimirlem27  38485  mblfinlem3  38497  mblfinlem4  38498  ismblfin  38499  itg2addnclem  38509  itg2addnclem2  38510  itg2gt0cn  38513  iblabsnclem  38521  ftc1anclem6  38536  areacirclem2  38547  areacirclem5  38550  areacirc  38551  mettrifi  38611  drngoi  38805  eldm4  39133  exanres2  39155  disjecxrn  39264  exeupre  39343  brcoss2  39374  br1cossres2  39382  eldmcoss2  39401  eldm1cossres2  39403  brcosscnv2  39415  erimeq2  39615  disjqmap  39679  disjlem19  39756  prter3  39859  islshpat  39994  lsatnle  40021  ellkr2  40068  lshpkr  40094  lkr0f2  40138  lduallkr3  40139  lkreqN  40147  cvrval2  40251  isat3  40284  glbconN  40354  hlrelat5N  40378  cvrval4N  40391  atlt  40414  1cvrco  40449  pmaple  40738  isline2  40751  isline4N  40754  elpaddn0  40777  elpadd2at2  40784  cdlemkid4  41911  dia0  42029  cdlemm10N  42095  dibglbN  42143  dihmeetlem4preN  42283  dochkrshp3  42365  dvh4dimlem  42420  lcfl5  42473  mapdpglem3  42652  mapdheq  42705  hdmap1eq  42778  hdmapval2lem  42808  hdmapoc  42908  hlhillcs  42935  lcmineqlem18  43016  dvdsexpb  43314  renegadd  43351  resubadd  43358  redivmuld  43424  mulgt0b1d  43464  fsuppssind  43543  fz1eqin  43718  diophin  43721  jm2.19  43938  rmxdiophlem  43960  pw2f1ocnv  43982  wepwsolem  43987  gicabl  44044  idomodle  44136  onsupmaxb  44184  cantnf2  44270  tfsconcatb0  44289  tfsnfin  44297  ntrclsfveq2  45005  ntrclsss  45007  ntrclsk4  45016  extoimad  45108  radcnvrat  45242  bcc0  45268  hashomiso  45952  supxrre3rnmpt  46361  clim2f  46568  clim2f2  46602  liminfreuzlem  46734  liminfltlem  46736  xlimmnflimsup2  46784  xlimpnfliminf2  46793  xlimlimsupleliminf  46795  opprb  48023  funbrafv2b  48151  dfafn5a  48152  leaddsuble  48289  mod2addne  48362  iccpartgtprec  48424  flsqrt  48600  dfeven2  48669  dfodd3  48670  lindslinindimp2lem4  49495  snlindsntor  49505  regt1loggt0  49570  elbigo2  49586  elbigolo1  49591  fldivexpfllog2  49599  nnlog2ge0lt1  49600  blenpw2m1  49613  naryfvalelwrdf  49667  isprsd  49985  resccatlem  50103  functhinclem1  50474  thincciso  50483  thinciso  50500  isinito2lem  50528  fulltermc  50541  prstcprs  50590  oduoppcciso  50596  postc  50599  lmdran  50701  cmdlan  50702