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  613  imordc  902  ifpnst  994  3anibar  1189  xor2dc  1432  bilukdc  1438  snelpwg  4296  prelpw  4299  reuhypd  4562  opelresi  5016  iota1  5293  funbrfv2b  5678  dffn5im  5679  fneqeql  5743  f1ompt  5786  dff13  5892  fliftcnv  5919  isotr  5940  isoini  5942  caovord3  6179  releldm2  6331  tpostpos  6410  nnsssuc  6648  nnaordi  6654  iserd  6706  ecdmn0m  6724  qliftel  6762  qliftfun  6764  qliftf  6767  ecopovsym  6778  pw2f1odclem  6995  mapen  7007  supisolem  7175  cnvti  7186  omp1eomlem  7261  ctssdc  7280  isomnimap  7304  ismkvmap  7321  iswomnimap  7333  netap  7440  2omotaplemap  7443  recmulnqg  7578  nqtri3or  7583  ltmnqg  7588  mullocprlem  7757  addextpr  7808  gt0srpr  7935  ltsosr  7951  ltasrg  7957  map2psrprg  7992  xrlenlt  8211  letri3  8227  subadd  8349  ltsubadd2  8580  lesubadd2  8582  suble  8587  ltsub23  8589  ltaddpos2  8600  ltsubpos  8601  subge02  8625  ltaddsublt  8718  reapneg  8744  apsym  8753  apti  8769  leltap  8772  ap0gt0  8787  divmulap  8822  divmulap3  8824  rec11rap  8858  ltdiv1  9015  ltdivmul2  9025  ledivmul2  9027  ltrec  9030  suprleubex  9101  nnle1eq1  9134  avgle1  9352  avgle2  9353  nn0le0eq0  9397  znnnlt1  9494  zleltp1  9502  elz2  9518  uzm1  9753  uzin  9755  difrp  9888  xrletri3  10000  xgepnf  10012  xltnegi  10031  xltadd1  10072  xposdif  10078  xleaddadd  10083  elioo5  10129  elfz5  10213  fzdifsuc  10277  elfzm11  10287  uzsplit  10288  elfzonelfzo  10436  qtri3or  10460  qavgle  10478  flqbi  10510  flqbi2  10511  fldiv4lem1div2uz2  10526  zmodid2  10574  q2submod  10607  sqap0  10828  lt2sq  10835  le2sq  10836  nn0opthlem1d  10942  bcval5  10985  zfz1isolemiso  11061  pfxsuffeqwrdeq  11230  shftfib  11334  mulreap  11375  caucvgrelemcau  11491  caucvgre  11492  elicc4abs  11605  abs2difabs  11619  cau4  11627  maxclpr  11733  negfi  11739  lemininf  11745  mul0inf  11752  xrlemininf  11782  xrminltinf  11783  clim2  11794  climeq  11810  fisumss  11903  fsumabs  11976  isumshft  12001  absefib  12282  dvdsval3  12302  dvdslelemd  12354  dvdsabseq  12358  dvdsflip  12362  dvdsssfz1  12363  zeo3  12379  ndvdsadd  12442  bitscmp  12469  dvdssq  12552  algcvgblem  12571  lcmdvds  12601  ncoprmgcdgt1b  12612  isprm3  12640  phiprmpw  12744  prmdiv  12757  pc11  12854  pcz  12855  pockthlem  12879  1arith  12890  ercpbllemg  13363  grpinvcnv  13601  eqger  13761  ablsubadd  13849  dvdsr02  14069  opprunitd  14074  unitsubm  14083  issubrg3  14211  aprval  14246  rnglidlmmgm  14460  znleval2  14618  discld  14810  isneip  14820  restopnb  14855  restopn2  14857  restdis  14858  lmbr2  14888  cnptoprest  14913  cnptoprest2  14914  tx1cn  14943  tx2cn  14944  txcnmpt  14947  txrest  14950  elbl2ps  15066  elbl2  15067  blcomps  15070  blcom  15071  xblpnfps  15072  xblpnf  15073  blpnf  15074  xmeter  15110  bdxmet  15175  metrest  15180  xmetxp  15181  metcn  15188  cncfcdm  15256  reefiso  15451  gausslemma2dlem0c  15730  lgseisenlem3  15751  lgsquadlem1  15756  m1lgs  15764  2lgsoddprmlem2  15785  ausgrusgrben  15966