Theorem bitr4d 191

Description: Deduction form of bitr4i 187. (Contributed by NM, 5-Aug-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 141	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 188	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitr2d  216  3bitr2rd  217  3bitr4d  220  3bitr4rd  221  mpbirand  445  mpbiran2d  446  bianabs  619  imordc  909  ifpnst  1001  3anibar  1196  xor2dc  1439  bilukdc  1445  snelpwg  4348  prelpw  4351  reuhypd  4615  opelresi  5072  iota1  5350  funbrfv2b  5744  dffn5im  5745  fneqeql  5811  f1ompt  5853  dff13  5967  fliftcnv  5994  isotr  6015  isoini  6017  caovord3  6256  releldm2  6412  tpostpos  6528  nnsssuc  6768  nnaordi  6774  iserd  6826  ecdmn0m  6844  qliftel  6882  qliftfun  6884  qliftf  6887  ecopovsym  6898  pw2f1odclem  7127  mapen  7139  suppeqfsuppbi  7288  supisolem  7341  cnvti  7352  omp1eomlem  7427  ctssdc  7446  isomnimap  7470  ismkvmap  7487  iswomnimap  7499  netap  7613  2omotaplemap  7616  recmulnqg  7751  nqtri3or  7756  ltmnqg  7761  mullocprlem  7930  addextpr  7981  gt0srpr  8108  ltsosr  8124  ltasrg  8130  map2psrprg  8165  xrlenlt  8383  letri3  8399  subadd  8522  ltsubadd2  8754  lesubadd2  8756  suble  8761  ltsub23  8763  ltaddpos2  8774  ltsubpos  8775  subge02  8799  ltaddsublt  8892  reapneg  8918  apsym  8927  apti  8943  leltap  8946  ap0gt0  8961  divmulap  8998  divmulap3  9000  rec11rap  9034  ltdiv1  9191  ltdivmul2  9201  ledivmul2  9203  ltrec  9206  suprleubex  9277  nnle1eq1  9310  avgle1  9528  avgle2  9529  nn0le0eq0  9573  znnnlt1  9674  zleltp1  9682  elz2  9698  uzm1  9935  uzin  9937  difrp  10075  xrletri3  10188  xgepnf  10200  xltnegi  10219  xltadd1  10260  xposdif  10266  xleaddadd  10271  elioo5  10317  elfz5  10402  fzdifsuc  10469  elfzm11  10479  uzsplit  10480  elfzonelfzo  10629  qtri3or  10656  qavgle  10674  flqbi  10706  flqbi2  10707  fldiv4lem1div2uz2  10722  zmodid2  10770  q2submod  10803  sqap0  11024  lt2sq  11031  le2sq  11032  nn0opthlem1d  11139  bcval5  11182  zfz1isolemiso  11272  pfxsuffeqwrdeq  11451  shftfib  11569  mulreap  11610  caucvgrelemcau  11727  caucvgre  11728  elicc4abs  11841  abs2difabs  11855  cau4  11863  maxclpr  11969  negfi  11975  lemininf  11981  mul0inf  11988  xrlemininf  12018  xrminltinf  12019  clim2  12030  climeq  12046  fisumss  12140  fsumabs  12213  isumshft  12238  absefib  12519  dvdsval3  12539  dvdslelemd  12591  dvdsabseq  12595  dvdsflip  12599  dvdsssfz1  12600  zeo3  12616  ndvdsadd  12679  bitscmp  12706  dvdssq  12789  algcvgblem  12808  lcmdvds  12838  ncoprmgcdgt1b  12849  isprm3  12877  phiprmpw  12981  prmdiv  12994  pc11  13091  pcz  13092  pockthlem  13116  1arith  13127  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemodife  13221  ballotfilemsima  13240  ballotfilemfrcn0  13254  ercpbllemg  13631  grpinvcnv  13853  eqger  14007  ablsubadd  14096  dvdsr02  14388  opprunitd  14393  unitsubm  14402  issubrg3  14531  aprval  14567  opprdrng  14596  rnglidlmmgm  14808  znleval2  14964  discld  15163  isneip  15173  restopnb  15208  restopn2  15210  restdis  15211  lmbr2  15241  cnptoprest  15266  cnptoprest2  15267  tx1cn  15296  tx2cn  15297  txcnmpt  15300  txrest  15303  elbl2ps  15419  elbl2  15420  blcomps  15423  blcom  15424  xblpnfps  15425  xblpnf  15426  blpnf  15427  xmeter  15463  bdxmet  15528  metrest  15533  xmetxp  15534  metcn  15541  cncfcdm  15609  reefiso  15804  gausslemma2dlem0c  16087  lgseisenlem3  16108  lgsquadlem1  16113  m1lgs  16121  2lgsoddprmlem2  16142  ausgrusgrben  16326  eupth2lemsfi  16636