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  1166  xor2dc  1400  bilukdc  1406  reuhypd  4483  opelresi  4930  iota1  5204  funbrfv2b  5573  dffn5im  5574  fneqeql  5637  f1ompt  5680  dff13  5782  fliftcnv  5809  isotr  5830  isoini  5832  caovord3  6062  releldm2  6200  tpostpos  6279  nnsssuc  6517  nnaordi  6523  iserd  6575  ecdmn0m  6591  qliftel  6629  qliftfun  6631  qliftf  6634  ecopovsym  6645  mapen  6860  supisolem  7021  cnvti  7032  omp1eomlem  7107  ctssdc  7126  isomnimap  7149  ismkvmap  7166  iswomnimap  7178  netap  7267  2omotaplemap  7270  recmulnqg  7404  nqtri3or  7409  ltmnqg  7414  mullocprlem  7583  addextpr  7634  gt0srpr  7761  ltsosr  7777  ltasrg  7783  map2psrprg  7818  xrlenlt  8036  letri3  8052  subadd  8174  ltsubadd2  8404  lesubadd2  8406  suble  8411  ltsub23  8413  ltaddpos2  8424  ltsubpos  8425  subge02  8449  ltaddsublt  8542  reapneg  8568  apsym  8577  apti  8593  leltap  8596  ap0gt0  8611  divmulap  8646  divmulap3  8648  rec11rap  8682  ltdiv1  8839  ltdivmul2  8849  ledivmul2  8851  ltrec  8854  suprleubex  8925  nnle1eq1  8957  avgle1  9173  avgle2  9174  nn0le0eq0  9218  znnnlt1  9315  zleltp1  9322  elz2  9338  uzm1  9572  uzin  9574  difrp  9706  xrletri3  9818  xgepnf  9830  xltnegi  9849  xltadd1  9890  xposdif  9896  xleaddadd  9901  elioo5  9947  elfz5  10031  fzdifsuc  10095  elfzm11  10105  uzsplit  10106  elfzonelfzo  10244  qtri3or  10257  qavgle  10273  flqbi  10304  flqbi2  10305  zmodid2  10366  q2submod  10399  sqap0  10601  lt2sq  10608  le2sq  10609  nn0opthlem1d  10714  bcval5  10757  zfz1isolemiso  10833  shftfib  10846  mulreap  10887  caucvgrelemcau  11003  caucvgre  11004  elicc4abs  11117  abs2difabs  11131  cau4  11139  maxclpr  11245  negfi  11250  lemininf  11256  mul0inf  11263  xrlemininf  11293  xrminltinf  11294  clim2  11305  climeq  11321  fisumss  11414  fsumabs  11487  isumshft  11512  absefib  11792  dvdsval3  11812  dvdslelemd  11863  dvdsabseq  11867  dvdsflip  11871  dvdsssfz1  11872  zeo3  11887  ndvdsadd  11950  dvdssq  12046  algcvgblem  12063  lcmdvds  12093  ncoprmgcdgt1b  12104  isprm3  12132  phiprmpw  12236  prmdiv  12249  pc11  12344  pcz  12345  pockthlem  12368  1arith  12379  ercpbllemg  12768  grpinvcnv  12965  eqger  13116  ablsubadd  13149  dvdsr02  13353  opprunitd  13358  unitsubm  13367  issubrg3  13467  aprval  13471  rnglidlmmgm  13685  discld  13932  isneip  13942  restopnb  13977  restopn2  13979  restdis  13980  lmbr2  14010  cnptoprest  14035  cnptoprest2  14036  tx1cn  14065  tx2cn  14066  txcnmpt  14069  txrest  14072  elbl2ps  14188  elbl2  14189  blcomps  14192  blcom  14193  xblpnfps  14194  xblpnf  14195  blpnf  14196  xmeter  14232  bdxmet  14297  metrest  14302  xmetxp  14303  metcn  14310  cncfcdm  14365  reefiso  14494  m1lgs  14748  2lgsoddprmlem2  14750