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  441  mpbiran2d  442  bianabs  615  imordc  905  ifpnst  997  3anibar  1192  xor2dc  1435  bilukdc  1441  snelpwg  4331  prelpw  4334  reuhypd  4597  opelresi  5054  iota1  5332  funbrfv2b  5726  dffn5im  5727  fneqeql  5791  f1ompt  5833  dff13  5947  fliftcnv  5974  isotr  5995  isoini  5997  caovord3  6236  releldm2  6392  tpostpos  6508  nnsssuc  6748  nnaordi  6754  iserd  6806  ecdmn0m  6824  qliftel  6862  qliftfun  6864  qliftf  6867  ecopovsym  6878  pw2f1odclem  7100  mapen  7112  suppeqfsuppbi  7261  supisolem  7312  cnvti  7323  omp1eomlem  7398  ctssdc  7417  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  netap  7584  2omotaplemap  7587  recmulnqg  7722  nqtri3or  7727  ltmnqg  7732  mullocprlem  7901  addextpr  7952  gt0srpr  8079  ltsosr  8095  ltasrg  8101  map2psrprg  8136  xrlenlt  8354  letri3  8370  subadd  8493  ltsubadd2  8725  lesubadd2  8727  suble  8732  ltsub23  8734  ltaddpos2  8745  ltsubpos  8746  subge02  8770  ltaddsublt  8863  reapneg  8889  apsym  8898  apti  8914  leltap  8917  ap0gt0  8932  divmulap  8969  divmulap3  8971  rec11rap  9005  ltdiv1  9162  ltdivmul2  9172  ledivmul2  9174  ltrec  9177  suprleubex  9248  nnle1eq1  9281  avgle1  9499  avgle2  9500  nn0le0eq0  9544  znnnlt1  9645  zleltp1  9653  elz2  9669  uzm1  9906  uzin  9908  difrp  10046  xrletri3  10159  xgepnf  10171  xltnegi  10190  xltadd1  10231  xposdif  10237  xleaddadd  10242  elioo5  10288  elfz5  10373  fzdifsuc  10440  elfzm11  10450  uzsplit  10451  elfzonelfzo  10600  qtri3or  10627  qavgle  10645  flqbi  10677  flqbi2  10678  fldiv4lem1div2uz2  10693  zmodid2  10741  q2submod  10774  sqap0  10995  lt2sq  11002  le2sq  11003  nn0opthlem1d  11110  bcval5  11153  zfz1isolemiso  11239  pfxsuffeqwrdeq  11418  shftfib  11536  mulreap  11577  caucvgrelemcau  11694  caucvgre  11695  elicc4abs  11808  abs2difabs  11822  cau4  11830  maxclpr  11936  negfi  11942  lemininf  11948  mul0inf  11955  xrlemininf  11985  xrminltinf  11986  clim2  11997  climeq  12013  fisumss  12107  fsumabs  12180  isumshft  12205  absefib  12486  dvdsval3  12506  dvdslelemd  12558  dvdsabseq  12562  dvdsflip  12566  dvdsssfz1  12567  zeo3  12583  ndvdsadd  12646  bitscmp  12673  dvdssq  12756  algcvgblem  12775  lcmdvds  12805  ncoprmgcdgt1b  12816  isprm3  12844  phiprmpw  12948  prmdiv  12961  pc11  13058  pcz  13059  pockthlem  13083  1arith  13094  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemodife  13188  ballotfilemsima  13207  ballotfilemfrcn0  13221  ercpbllemg  13598  grpinvcnv  13827  eqger  13981  ablsubadd  14069  dvdsr02  14354  opprunitd  14359  unitsubm  14368  issubrg3  14497  aprval  14533  opprdrng  14562  rnglidlmmgm  14774  znleval2  14932  discld  15131  isneip  15141  restopnb  15176  restopn2  15178  restdis  15179  lmbr2  15209  cnptoprest  15234  cnptoprest2  15235  tx1cn  15264  tx2cn  15265  txcnmpt  15268  txrest  15271  elbl2ps  15387  elbl2  15388  blcomps  15391  blcom  15392  xblpnfps  15393  xblpnf  15394  blpnf  15395  xmeter  15431  bdxmet  15496  metrest  15501  xmetxp  15502  metcn  15509  cncfcdm  15577  reefiso  15772  gausslemma2dlem0c  16054  lgseisenlem3  16075  lgsquadlem1  16080  m1lgs  16088  2lgsoddprmlem2  16109  ausgrusgrben  16293  eupth2lemsfi  16603