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  4479  issn  4792  disjprg  5099  reuhypd  5384  snelpwg  5418  ordtri3  6394  ordsssuc  6449  iota1  6512  funbrfv2b  6935  dffn5  6936  feqmptdf  6948  unima  6953  dmfco  6974  fneqeql  7038  f1ompt  7104  dff13  7251  fliftcnv  7312  soisores  7328  isotr  7337  isoini  7339  caovord3  7627  releldm2  8040  fimaproj  8133  brtpos  8233  tpostpos  8244  oe1m  8532  oawordri  8537  oalimcl  8547  omlimcl  8565  omabs  8639  iserd  8723  qliftel  8800  qliftfun  8802  qliftf  8805  ecopovsym  8819  pw2f1olem  9079  mapen  9139  findcard3  9253  tfsnfin2  9330  suppeqfsuppbi  9349  mapfien  9378  supisolem  9444  cantnflem1  9668  wemapwe  9676  rankr1clem  9802  rankr1c  9803  ranklim  9826  r1pwALT  9828  r1pwcl  9829  isfin1-2  10387  isfin1-4  10389  fin71num  10399  axdc3lem2  10453  infinfg  10574  ltmnq  10981  prlem936  11056  ltsosr  11103  ltasr  11109  xrlenlt  11298  ltxrlt  11304  letri3  11319  ne0gt0  11339  subadd  11484  ltsubadd2  11709  lesubadd2  11711  suble  11716  ltsub23  11718  ltaddpos2  11729  ltsubpos  11730  subge02  11754  ltord2  11767  leord2  11768  ltaddsublt  11865  divmul  11899  divmul3  11901  rec11r  11938  ltdiv1  12103  ltdivmul2  12116  ledivmul2  12118  ltrec  12121  ltdiv2  12125  negfi  12188  negiso  12219  nnle1eq1  12290  avgle1  12508  avgle2  12509  avgle  12510  nn0le0eq0  12556  elz2  12633  znnnlt1  12645  zleltp1  12669  difrp  13082  xrltlen  13197  dfle2  13198  xrletri3  13205  xgepnf  13217  xlemnf  13219  qbtwnre  13251  xltnegi  13268  supxrre  13379  infxrre  13389  elioo5  13456  elfz5  13570  elfzm11  13650  predfz  13708  flbi  13877  flbi2  13878  fldiv4lem1div2uz2  13897  fznnfl  13923  zmodid2  13960  2submod  13996  lt2sq  14197  le2sq  14198  sqlecan  14273  bcval5  14382  pfxsuffeqwrdeq  14767  shftfib  15145  sgn3da  15174  mulre  15208  cnpart  15327  01sqrexlem6  15334  sqrmo  15338  elicc4abs  15407  abs2difabs  15422  cau4  15444  limsupgre  15568  clim2  15591  ello1mpt2  15609  lo1resb  15651  o1resb  15653  climeq  15654  climmpt2  15660  isercoll  15755  caucvgb  15767  fsumabs  15888  isumshft  15928  geomulcvg  15965  absefib  16286  dvdsval3  16346  addmulmodb  16355  dvdsabseq  16403  dvdsflip  16407  dvdsssfz1  16408  mod2eq1n2dvds  16437  ndvdsadd  16500  bitscmp  16528  smupvallem  16573  dvdssq  16657  lcmdvds  16698  ncoprmgcdgt1b  16741  isprm3  16773  isprm5  16798  phiprmpw  16867  prmdiv  16876  pc11  16972  pcz  16973  pockthlem  16997  prmreclem2  17009  prmreclem4  17011  prmreclem6  17013  1arith  17019  vdwapun  17066  rami  17107  ramcl  17121  pwsle  17578  ercpbllem  17634  invsym  17851  funcres2c  17992  latnle  18561  grpinvcnv  19130  subgacs  19284  eqger  19303  ghmqusker  19414  gexdvds2  19712  pgpfi1  19722  pgpfi  19732  lsmass  19796  lssnle  19801  lsmdisj3b  19817  lsmhash  19832  ablsubadd  19936  gsumval3lem2  20033  subgdmdprd  20163  pgpfac1lem2  20204  dvdsr02  20513  issubrg3  20762  isdomn3  20876  drngid2  20919  sdrgunit  20962  sdrgacs  20967  lssacs  21151  prmirred  21687  chrdvds  21739  chrcong  21740  chrnzr  21743  znleval  21767  znleval2  21768  cygznlem3  21782  frlmbas  21968  elfilspd  22016  lindfmm  22040  islindf4  22051  islindf5  22052  psrbaglefi  22141  coe1mul2lem1  22493  mdetunilem9  22842  matunitlindflem1  22901  matunitlindflem2  22902  matunitlindf  22903  isneip  23330  neiptopnei  23357  lpdifsn  23368  restopnb  23400  restopn2  23402  restdis  23403  restperf  23409  lmbr2  23484  cncls2  23498  cnprest  23514  cnprest2  23515  iscnrm2  23563  ist0-2  23569  ist1-3  23574  ishaus2  23576  cmpfi  23633  dfconn2  23644  1stccnp  23688  subislly  23707  hausmapdom  23726  tx1cn  23835  tx2cn  23836  txcnmpt  23850  txrest  23857  hauseqlcld  23872  tgqtop  23938  qtopcld  23939  ordthmeolem  24027  trfil2  24113  trfil3  24114  trnei  24118  ufildr  24157  fmfg  24175  rnelfm  24179  fmfnfm  24184  elflim  24197  flimrest  24209  cnflf  24228  cnflf2  24229  ptcmplem2  24279  ghmcnp  24341  tsmssubm  24369  iscfilu  24513  xmetgt0  24584  prdsxmetlem  24594  blcomps  24619  blcom  24620  xblpnfps  24621  xblpnf  24622  blpnf  24623  xmeter  24659  setsxms  24705  imasf1obl  24714  stdbdbl  24743  metrest  24750  metuel2  24791  dscopn  24799  xrtgioo  25033  metdstri  25078  cnmpopc  25156  iihalf2  25161  icopnfhmeo  25171  evth2  25188  lmmbr3  25488  iscau3  25506  metcld  25534  cfilucfil3  25548  srabn  25588  rrxmet  25636  minveclem4  25660  evthicc2  25688  ovolgelb  25708  shft2rab  25736  ovolshftlem1  25737  sca2rab  25740  ovolscalem1  25741  ioombl1lem4  25789  mbfmulc2lem  25875  ismbf3d  25882  mbfsup  25892  mbfinf  25893  i1f1lem  25917  i1fmulclem  25930  mbfi1fseqlem4  25946  itg2seq  25970  ditgneg  26084  limcdif  26103  limcnlp  26105  cnplimc  26114  rolle  26217  mvth  26219  dvne0  26238  lhop1lem  26240  itgsubst  26276  mdegle0  26302  deg1leb  26320  deg1le0  26336  q1peqb  26381  coemulhi  26480  dgrlt  26492  plydivlem3  26525  vieta1lem2  26543  aannenlem1  26564  ulmres  26624  reefiso  26684  pilem3  26689  ellogdm  26876  root1eq1  26992  angpieqvdlem  27065  angpieqvdlem2  27066  quad2  27076  1cubr  27079  quart  27098  rlimcnp  27202  wilthlem2  27305  isppw  27350  dvdsflsumcom  27424  fsumvma  27449  logfac2  27453  chpchtsum  27455  dchrmulcl  27485  dchrresb  27495  bclbnd  27516  bposlem1  27520  bposlem5  27524  gausslemma2dlem0c  27594  lgsquadlem1  27616  m1lgs  27624  2lgsoddprmlem2  27645  dchrisumlem3  27727  dchrisum0lem1  27752  ltsval2  27892  noextenddif  27904  lesloe  27990  lestri3  27991  eqcuts  28050  elmade2  28123  ltadds1  28257  negsunif  28320  ltsubs1  28341  ltsubadds2d  28355  mulsproplem12  28392  ltmuls2  28436  ltmuls1d  28438  divmulsw  28458  ltdivmuls2wd  28465  oniso  28536  n0subs  28628  n0lesltp1  28631  elzn0s  28663  avglts1d  28718  avglts2d  28719  bdaypw2n0bndlem  28728  z12sge0  28748  dfz12s2  28753  elreno2  28760  tgjustr  28815  trgcgrg  28857  lnrot1  28970  islnopp  29094  elplng  29137  plngcplem  29142  ismidb  29162  islmib  29171  axsegconlem6  29379  axeuclidlem  29419  axcontlem2  29422  axcontlem4  29424  axcontlem12  29432  lfuhgr2  29606  ausgrusgrb  29625  nb3grpr2  29843  cplgr2v  29892  umgr2v2enb1  29986  crctcsh  30292  clwwlknonwwlknonb  30576  eupth2lems  30718  nmoreltpnf  31250  isblo2  31264  nmlnogt0  31278  phoeqi  31338  ubthlem2  31352  hire  31575  normgt0  31608  ho01i  32309  ho02i  32310  hoeq1  32311  hoeq2  32312  nmopreltpnf  32350  adjeq  32416  leop  32604  leopmul2i  32616  pjnormssi  32649  pjimai  32657  jplem1  32749  mddmd2  32790  mdslmd1lem1  32806  mdslmd1lem2  32807  superpos  32835  atnssm0  32857  dmdbr5ati  32903  disjunsn  33067  fcoinvbr  33078  ofpreima  33138  funcnv5mpt  33140  suppiniseg  33158  isoun  33174  fpwrelmapffslem  33203  fpwrelmap  33204  iocinioc2  33250  xrdifh  33251  nndiffz1  33257  xdivmul  33370  cntzsnid  33520  cntrval2  33611  isarchi2  33625  isunitc  33681  erler  33705  rlocisunit  33716  elrsp  33806  lsmsnpridl  33829  lsmssass  33831  esplyind  34085  finexttrb  34175  algextdeglem6  34232  algextdeglem7  34233  smatrcl  34306  rhmpreimacnlem  34394  sqsscirc2  34419  xrmulc1cn  34440  esumfsup  34580  1stmbfm  34771  2ndmbfm  34772  mbfmcnt  34779  eulerpartlems  34871  eulerpartlemd  34877  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemsima  35027  ballotlemfrcn0  35041  reprinfz1  35130  reprdifc  35135  bnj1173  35511  fineqvnttrclse  35650  kardcard2  35692  vonf1wev  35705  vonf1owevOLD  35707  zltp1ne  35714  erdszelem7  35776  erdszelem9  35778  iscvm  35838  cvmlift3lem4  35901  rexxfr3dALT  36218  fscgr  36660  seglelin  36696  btwnoutside  36705  lineunray  36727  cldbnd  36945  isfne4  36959  fneval  36971  filnetlem4  37000  nndivsub  37076  bj-gabima  37684  dfgcd3  38076  fvineqsneu  38165  wl-sbhbt  38317  wl-sbcom2d  38324  wl-sbalnae  38325  sin2h  38364  cos2h  38365  ptrest  38368  poimirlem3  38372  poimirlem4  38373  poimirlem22  38391  poimirlem27  38396  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  itg2addnclem  38420  itg2addnclem2  38421  itg2gt0cn  38424  iblabsnclem  38432  ftc1anclem6  38447  areacirclem2  38458  areacirclem5  38461  areacirc  38462  mettrifi  38507  drngoi  38701  eldm4  39029  exanres2  39051  disjecxrn  39160  exeupre  39239  brcoss2  39270  br1cossres2  39278  eldmcoss2  39297  eldm1cossres2  39299  brcosscnv2  39311  erimeq2  39511  disjqmap  39575  disjlem19  39652  prter3  39755  islshpat  39890  lsatnle  39917  ellkr2  39964  lshpkr  39990  lkr0f2  40034  lduallkr3  40035  lkreqN  40043  cvrval2  40147  isat3  40180  glbconN  40250  hlrelat5N  40274  cvrval4N  40287  atlt  40310  1cvrco  40345  pmaple  40634  isline2  40647  isline4N  40650  elpaddn0  40673  elpadd2at2  40680  cdlemkid4  41807  dia0  41925  cdlemm10N  41991  dibglbN  42039  dihmeetlem4preN  42179  dochkrshp3  42261  dvh4dimlem  42316  lcfl5  42369  mapdpglem3  42548  mapdheq  42601  hdmap1eq  42674  hdmapval2lem  42704  hdmapoc  42804  hlhillcs  42831  lcmineqlem18  42912  dvdsexpb  43210  renegadd  43247  resubadd  43254  redivmuld  43320  mulgt0b1d  43360  fsuppssind  43439  fz1eqin  43614  diophin  43617  jm2.19  43834  rmxdiophlem  43856  pw2f1ocnv  43878  wepwsolem  43883  gicabl  43940  idomodle  44032  onsupmaxb  44080  cantnf2  44166  tfsconcatb0  44185  tfsnfin  44193  ntrclsfveq2  44901  ntrclsss  44903  ntrclsk4  44912  extoimad  45004  radcnvrat  45138  bcc0  45164  hashomiso  45848  supxrre3rnmpt  46257  clim2f  46464  clim2f2  46498  liminfreuzlem  46630  liminfltlem  46632  xlimmnflimsup2  46680  xlimpnfliminf2  46689  xlimlimsupleliminf  46691  opprb  47919  funbrafv2b  48047  dfafn5a  48048  leaddsuble  48185  mod2addne  48258  iccpartgtprec  48320  flsqrt  48496  dfeven2  48565  dfodd3  48566  lindslinindimp2lem4  49391  snlindsntor  49401  regt1loggt0  49466  elbigo2  49482  elbigolo1  49487  fldivexpfllog2  49495  nnlog2ge0lt1  49496  blenpw2m1  49509  naryfvalelwrdf  49563  isprsd  49881  resccatlem  49999  functhinclem1  50370  thincciso  50379  thinciso  50396  isinito2lem  50424  fulltermc  50437  prstcprs  50486  oduoppcciso  50492  postc  50495  lmdran  50597  cmdlan  50598