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  4308  prelpw  4311  reuhypd  4574  opelresi  5030  iota1  5308  funbrfv2b  5699  dffn5im  5700  fneqeql  5764  f1ompt  5806  dff13  5919  fliftcnv  5946  isotr  5967  isoini  5969  caovord3  6206  releldm2  6357  tpostpos  6473  nnsssuc  6713  nnaordi  6719  iserd  6771  ecdmn0m  6789  qliftel  6827  qliftfun  6829  qliftf  6832  ecopovsym  6843  pw2f1odclem  7063  mapen  7075  supisolem  7250  cnvti  7261  omp1eomlem  7336  ctssdc  7355  isomnimap  7379  ismkvmap  7396  iswomnimap  7408  netap  7516  2omotaplemap  7519  recmulnqg  7654  nqtri3or  7659  ltmnqg  7664  mullocprlem  7833  addextpr  7884  gt0srpr  8011  ltsosr  8027  ltasrg  8033  map2psrprg  8068  xrlenlt  8287  letri3  8303  subadd  8425  ltsubadd2  8656  lesubadd2  8658  suble  8663  ltsub23  8665  ltaddpos2  8676  ltsubpos  8677  subge02  8701  ltaddsublt  8794  reapneg  8820  apsym  8829  apti  8845  leltap  8848  ap0gt0  8863  divmulap  8898  divmulap3  8900  rec11rap  8934  ltdiv1  9091  ltdivmul2  9101  ledivmul2  9103  ltrec  9106  suprleubex  9177  nnle1eq1  9210  avgle1  9428  avgle2  9429  nn0le0eq0  9473  znnnlt1  9570  zleltp1  9578  elz2  9594  uzm1  9830  uzin  9832  difrp  9970  xrletri3  10082  xgepnf  10094  xltnegi  10113  xltadd1  10154  xposdif  10160  xleaddadd  10165  elioo5  10211  elfz5  10295  fzdifsuc  10359  elfzm11  10369  uzsplit  10370  elfzonelfzo  10519  qtri3or  10544  qavgle  10562  flqbi  10594  flqbi2  10595  fldiv4lem1div2uz2  10610  zmodid2  10658  q2submod  10691  sqap0  10912  lt2sq  10919  le2sq  10920  nn0opthlem1d  11026  bcval5  11069  zfz1isolemiso  11147  pfxsuffeqwrdeq  11326  shftfib  11444  mulreap  11485  caucvgrelemcau  11601  caucvgre  11602  elicc4abs  11715  abs2difabs  11729  cau4  11737  maxclpr  11843  negfi  11849  lemininf  11855  mul0inf  11862  xrlemininf  11892  xrminltinf  11893  clim2  11904  climeq  11920  fisumss  12014  fsumabs  12087  isumshft  12112  absefib  12393  dvdsval3  12413  dvdslelemd  12465  dvdsabseq  12469  dvdsflip  12473  dvdsssfz1  12474  zeo3  12490  ndvdsadd  12553  bitscmp  12580  dvdssq  12663  algcvgblem  12682  lcmdvds  12712  ncoprmgcdgt1b  12723  isprm3  12751  phiprmpw  12855  prmdiv  12868  pc11  12965  pcz  12966  pockthlem  12990  1arith  13001  ercpbllemg  13474  grpinvcnv  13712  eqger  13872  ablsubadd  13960  dvdsr02  14181  opprunitd  14186  unitsubm  14195  issubrg3  14323  aprval  14358  rnglidlmmgm  14572  znleval2  14730  discld  14927  isneip  14937  restopnb  14972  restopn2  14974  restdis  14975  lmbr2  15005  cnptoprest  15030  cnptoprest2  15031  tx1cn  15060  tx2cn  15061  txcnmpt  15064  txrest  15067  elbl2ps  15183  elbl2  15184  blcomps  15187  blcom  15188  xblpnfps  15189  xblpnf  15190  blpnf  15191  xmeter  15227  bdxmet  15292  metrest  15297  xmetxp  15298  metcn  15305  cncfcdm  15373  reefiso  15568  gausslemma2dlem0c  15850  lgseisenlem3  15871  lgsquadlem1  15876  m1lgs  15884  2lgsoddprmlem2  15905  ausgrusgrben  16089  eupth2lemsfi  16399