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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  4352  prelpw  4355  reuhypd  4619  opelresi  5076  iota1  5355  funbrfv2b  5750  dffn5im  5751  fneqeql  5820  f1ompt  5862  dff13  5977  fliftcnv  6004  isotr  6025  isoini  6027  caovord3  6266  releldm2  6423  suppinisegdc  6513  tpostpos  6540  nnsssuc  6780  nnaordi  6786  iserd  6838  ecdmn0m  6856  qliftel  6894  qliftfun  6896  qliftf  6899  ecopovsym  6910  pw2f1odclem  7140  mapen  7152  relresfin  7270  supisolem  7355  cnvti  7366  omp1eomlem  7441  ctssdc  7460  isomnimap  7484  ismkvmap  7501  iswomnimap  7513  netap  7627  2omotaplemap  7630  recmulnqg  7765  nqtri3or  7770  ltmnqg  7775  mullocprlem  7944  addextpr  7995  gt0srpr  8122  ltsosr  8138  ltasrg  8144  map2psrprg  8179  xrlenlt  8397  letri3  8413  subadd  8537  ltsubadd2  8769  lesubadd2  8771  suble  8776  ltsub23  8778  ltaddpos2  8789  ltsubpos  8790  subge02  8814  ltaddsublt  8908  reapneg  8934  apsym  8943  apti  8959  leltap  8962  ap0gt0  8977  divmulap  9014  divmulap3  9016  rec11rap  9050  ltdiv1  9207  ltdivmul2  9217  ledivmul2  9219  ltrec  9222  suprleubex  9293  nnle1eq1  9338  avgle1  9558  avgle2  9559  nn0le0eq0  9603  znnnlt1  9702  zleltp1  9710  elz2  9726  uzm1  9969  uzin  9971  difrp  10110  xrletri3  10223  xgepnf  10235  xltnegi  10254  xltadd1  10295  xposdif  10301  xleaddadd  10306  elioo5  10352  elfz5  10437  fzdifsuc  10505  elfzm11  10515  uzsplit  10516  elfzonelfzo  10665  qtri3or  10692  qavgle  10710  flqbi  10746  flqbi2  10747  fldiv4lem1div2uz2  10762  zmodid2  10810  q2submod  10843  sqap0  11064  lt2sq  11071  le2sq  11072  nn0opthlem1d  11180  bcval5  11223  zfz1isolemiso  11313  pfxsuffeqwrdeq  11492  shftfib  11610  mulreap  11651  caucvgrelemcau  11768  caucvgre  11769  elicc4abs  11883  abs2difabs  11897  cau4  11905  maxclpr  12011  negfi  12017  lemininf  12024  mul0inf  12032  xrlemininf  12062  xrminltinf  12063  clim2  12074  climeq  12090  fisumss  12184  fsumabs  12257  isumshft  12282  absefib  12563  dvdsval3  12583  dvdslelemd  12635  dvdsabseq  12639  dvdsflip  12643  dvdsssfz1  12644  zeo3  12660  ndvdsadd  12723  bitscmp  12750  dvdssq  12833  algcvgblem  12852  lcmdvds  12882  ncoprmgcdgt1b  12893  isprm3  12921  phiprmpw  13029  prmdiv  13042  pc11  13139  pcz  13140  pockthlem  13164  1arith  13175  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemsima  13317  ballotfilemfrcn0  13331  ercpbllemg  13710  grpinvcnv  13932  eqger  14086  ablsubadd  14206  dvdsr02  14521  opprunitd  14526  unitsubm  14535  issubrg3  14664  aprval  14700  opprdrng  14729  rnglidlmmgm  14942  znleval2  15098  discld  15395  isneip  15405  restopnb  15440  restopn2  15442  restdis  15443  lmbr2  15473  cnptoprest  15498  cnptoprest2  15499  tx1cn  15528  tx2cn  15529  txcnmpt  15532  txrest  15535  elbl2ps  15651  elbl2  15652  blcomps  15655  blcom  15656  xblpnfps  15657  xblpnf  15658  blpnf  15659  xmeter  15695  bdxmet  15760  metrest  15765  xmetxp  15766  metcn  15773  cncfcdm  15841  reefiso  16036  bclbnd  16340  bposlem1  16344  bposlem5  16348  bpos  16353  gausslemma2dlem0c  16408  lgseisenlem3  16429  lgsquadlem1  16434  m1lgs  16442  2lgsoddprmlem2  16463  ausgrusgrben  16647  eupth2lemsfi  16957