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  611  imordc  898  3anibar  1167  xor2dc  1401  bilukdc  1407  reuhypd  4507  opelresi  4958  iota1  5234  funbrfv2b  5608  dffn5im  5609  fneqeql  5673  f1ompt  5716  dff13  5818  fliftcnv  5845  isotr  5866  isoini  5868  caovord3  6101  releldm2  6252  tpostpos  6331  nnsssuc  6569  nnaordi  6575  iserd  6627  ecdmn0m  6645  qliftel  6683  qliftfun  6685  qliftf  6688  ecopovsym  6699  pw2f1odclem  6904  mapen  6916  supisolem  7083  cnvti  7094  omp1eomlem  7169  ctssdc  7188  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  netap  7339  2omotaplemap  7342  recmulnqg  7477  nqtri3or  7482  ltmnqg  7487  mullocprlem  7656  addextpr  7707  gt0srpr  7834  ltsosr  7850  ltasrg  7856  map2psrprg  7891  xrlenlt  8110  letri3  8126  subadd  8248  ltsubadd2  8479  lesubadd2  8481  suble  8486  ltsub23  8488  ltaddpos2  8499  ltsubpos  8500  subge02  8524  ltaddsublt  8617  reapneg  8643  apsym  8652  apti  8668  leltap  8671  ap0gt0  8686  divmulap  8721  divmulap3  8723  rec11rap  8757  ltdiv1  8914  ltdivmul2  8924  ledivmul2  8926  ltrec  8929  suprleubex  9000  nnle1eq1  9033  avgle1  9251  avgle2  9252  nn0le0eq0  9296  znnnlt1  9393  zleltp1  9400  elz2  9416  uzm1  9651  uzin  9653  difrp  9786  xrletri3  9898  xgepnf  9910  xltnegi  9929  xltadd1  9970  xposdif  9976  xleaddadd  9981  elioo5  10027  elfz5  10111  fzdifsuc  10175  elfzm11  10185  uzsplit  10186  elfzonelfzo  10325  qtri3or  10349  qavgle  10367  flqbi  10399  flqbi2  10400  fldiv4lem1div2uz2  10415  zmodid2  10463  q2submod  10496  sqap0  10717  lt2sq  10724  le2sq  10725  nn0opthlem1d  10831  bcval5  10874  zfz1isolemiso  10950  shftfib  11007  mulreap  11048  caucvgrelemcau  11164  caucvgre  11165  elicc4abs  11278  abs2difabs  11292  cau4  11300  maxclpr  11406  negfi  11412  lemininf  11418  mul0inf  11425  xrlemininf  11455  xrminltinf  11456  clim2  11467  climeq  11483  fisumss  11576  fsumabs  11649  isumshft  11674  absefib  11955  dvdsval3  11975  dvdslelemd  12027  dvdsabseq  12031  dvdsflip  12035  dvdsssfz1  12036  zeo3  12052  ndvdsadd  12115  bitscmp  12142  dvdssq  12225  algcvgblem  12244  lcmdvds  12274  ncoprmgcdgt1b  12285  isprm3  12313  phiprmpw  12417  prmdiv  12430  pc11  12527  pcz  12528  pockthlem  12552  1arith  12563  ercpbllemg  13034  grpinvcnv  13272  eqger  13432  ablsubadd  13520  dvdsr02  13739  opprunitd  13744  unitsubm  13753  issubrg3  13881  aprval  13916  rnglidlmmgm  14130  znleval2  14288  discld  14458  isneip  14468  restopnb  14503  restopn2  14505  restdis  14506  lmbr2  14536  cnptoprest  14561  cnptoprest2  14562  tx1cn  14591  tx2cn  14592  txcnmpt  14595  txrest  14598  elbl2ps  14714  elbl2  14715  blcomps  14718  blcom  14719  xblpnfps  14720  xblpnf  14721  blpnf  14722  xmeter  14758  bdxmet  14823  metrest  14828  xmetxp  14829  metcn  14836  cncfcdm  14904  reefiso  15099  gausslemma2dlem0c  15378  lgseisenlem3  15399  lgsquadlem1  15404  m1lgs  15412  2lgsoddprmlem2  15433