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  5968  fliftcnv  5995  isotr  6016  isoini  6018  caovord3  6257  releldm2  6413  tpostpos  6529  nnsssuc  6769  nnaordi  6775  iserd  6827  ecdmn0m  6845  qliftel  6883  qliftfun  6885  qliftf  6888  ecopovsym  6899  pw2f1odclem  7128  mapen  7140  suppeqfsuppbi  7289  supisolem  7342  cnvti  7353  omp1eomlem  7428  ctssdc  7447  isomnimap  7471  ismkvmap  7488  iswomnimap  7500  netap  7614  2omotaplemap  7617  recmulnqg  7752  nqtri3or  7757  ltmnqg  7762  mullocprlem  7931  addextpr  7982  gt0srpr  8109  ltsosr  8125  ltasrg  8131  map2psrprg  8166  xrlenlt  8384  letri3  8400  subadd  8523  ltsubadd2  8755  lesubadd2  8757  suble  8762  ltsub23  8764  ltaddpos2  8775  ltsubpos  8776  subge02  8800  ltaddsublt  8893  reapneg  8919  apsym  8928  apti  8944  leltap  8947  ap0gt0  8962  divmulap  8999  divmulap3  9001  rec11rap  9035  ltdiv1  9192  ltdivmul2  9202  ledivmul2  9204  ltrec  9207  suprleubex  9278  nnle1eq1  9311  avgle1  9529  avgle2  9530  nn0le0eq0  9574  znnnlt1  9675  zleltp1  9683  elz2  9699  uzm1  9936  uzin  9938  difrp  10076  xrletri3  10189  xgepnf  10201  xltnegi  10220  xltadd1  10261  xposdif  10267  xleaddadd  10272  elioo5  10318  elfz5  10403  fzdifsuc  10471  elfzm11  10481  uzsplit  10482  elfzonelfzo  10631  qtri3or  10658  qavgle  10676  flqbi  10708  flqbi2  10709  fldiv4lem1div2uz2  10724  zmodid2  10772  q2submod  10805  sqap0  11026  lt2sq  11033  le2sq  11034  nn0opthlem1d  11141  bcval5  11184  zfz1isolemiso  11274  pfxsuffeqwrdeq  11453  shftfib  11571  mulreap  11612  caucvgrelemcau  11729  caucvgre  11730  elicc4abs  11843  abs2difabs  11857  cau4  11865  maxclpr  11971  negfi  11977  lemininf  11983  mul0inf  11990  xrlemininf  12020  xrminltinf  12021  clim2  12032  climeq  12048  fisumss  12142  fsumabs  12215  isumshft  12240  absefib  12521  dvdsval3  12541  dvdslelemd  12593  dvdsabseq  12597  dvdsflip  12601  dvdsssfz1  12602  zeo3  12618  ndvdsadd  12681  bitscmp  12708  dvdssq  12791  algcvgblem  12810  lcmdvds  12840  ncoprmgcdgt1b  12851  isprm3  12879  phiprmpw  12983  prmdiv  12996  pc11  13093  pcz  13094  pockthlem  13118  1arith  13129  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemodife  13223  ballotfilemsima  13242  ballotfilemfrcn0  13256  ercpbllemg  13634  grpinvcnv  13856  eqger  14010  ablsubadd  14099  dvdsr02  14395  opprunitd  14400  unitsubm  14409  issubrg3  14538  aprval  14574  opprdrng  14603  rnglidlmmgm  14816  znleval2  14972  discld  15220  isneip  15230  restopnb  15265  restopn2  15267  restdis  15268  lmbr2  15298  cnptoprest  15323  cnptoprest2  15324  tx1cn  15353  tx2cn  15354  txcnmpt  15357  txrest  15360  elbl2ps  15476  elbl2  15477  blcomps  15480  blcom  15481  xblpnfps  15482  xblpnf  15483  blpnf  15484  xmeter  15520  bdxmet  15585  metrest  15590  xmetxp  15591  metcn  15598  cncfcdm  15666  reefiso  15861  gausslemma2dlem0c  16153  lgseisenlem3  16174  lgsquadlem1  16179  m1lgs  16187  2lgsoddprmlem2  16208  ausgrusgrben  16392  eupth2lemsfi  16702