Theorem bitr4d 190

Description: Deduction form of bitr4i 186. (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 140	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 187	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2d  215  3bitr2rd  216  3bitr4d  219  3bitr4rd  220  mpbirand  439  mpbiran2d  440  bianabs  606  imordc  892  3anibar  1160  xor2dc  1385  bilukdc  1391  reuhypd  4454  opelresi  4900  iota1  5172  funbrfv2b  5539  dffn5im  5540  fneqeql  5602  f1ompt  5645  dff13  5745  fliftcnv  5772  isotr  5793  isoini  5795  caovord3  6024  releldm2  6162  tpostpos  6241  nnsssuc  6479  nnaordi  6485  iserd  6537  ecdmn0m  6553  qliftel  6591  qliftfun  6593  qliftf  6596  ecopovsym  6607  mapen  6822  supisolem  6983  cnvti  6994  omp1eomlem  7069  ctssdc  7088  isomnimap  7111  ismkvmap  7128  iswomnimap  7140  recmulnqg  7346  nqtri3or  7351  ltmnqg  7356  mullocprlem  7525  addextpr  7576  gt0srpr  7703  ltsosr  7719  ltasrg  7725  map2psrprg  7760  xrlenlt  7977  letri3  7993  subadd  8115  ltsubadd2  8345  lesubadd2  8347  suble  8352  ltsub23  8354  ltaddpos2  8365  ltsubpos  8366  subge02  8390  ltaddsublt  8483  reapneg  8509  apsym  8518  apti  8534  leltap  8537  ap0gt0  8552  divmulap  8585  divmulap3  8587  rec11rap  8621  ltdiv1  8777  ltdivmul2  8787  ledivmul2  8789  ltrec  8792  suprleubex  8863  nnle1eq1  8895  avgle1  9111  avgle2  9112  nn0le0eq0  9156  znnnlt1  9253  zleltp1  9260  elz2  9276  uzm1  9510  uzin  9512  difrp  9642  xrletri3  9754  xgepnf  9766  xltnegi  9785  xltadd1  9826  xposdif  9832  xleaddadd  9837  elioo5  9883  elfz5  9966  fzdifsuc  10030  elfzm11  10040  uzsplit  10041  elfzonelfzo  10179  qtri3or  10192  qavgle  10208  flqbi  10239  flqbi2  10240  zmodid2  10301  q2submod  10334  sqap0  10535  lt2sq  10542  le2sq  10543  nn0opthlem1d  10647  bcval5  10690  zfz1isolemiso  10767  shftfib  10780  mulreap  10821  caucvgrelemcau  10937  caucvgre  10938  elicc4abs  11051  abs2difabs  11065  cau4  11073  maxclpr  11179  negfi  11184  lemininf  11190  mul0inf  11197  xrlemininf  11227  xrminltinf  11228  clim2  11239  climeq  11255  fisumss  11348  fsumabs  11421  isumshft  11446  absefib  11726  dvdsval3  11746  dvdslelemd  11796  dvdsabseq  11800  dvdsflip  11804  dvdsssfz1  11805  zeo3  11820  ndvdsadd  11883  dvdssq  11979  algcvgblem  11996  lcmdvds  12026  ncoprmgcdgt1b  12037  isprm3  12065  phiprmpw  12169  prmdiv  12182  pc11  12277  pcz  12278  pockthlem  12301  1arith  12312  discld  12895  isneip  12905  restopnb  12940  restopn2  12942  restdis  12943  lmbr2  12973  cnptoprest  12998  cnptoprest2  12999  tx1cn  13028  tx2cn  13029  txcnmpt  13032  txrest  13035  elbl2ps  13151  elbl2  13152  blcomps  13155  blcom  13156  xblpnfps  13157  xblpnf  13158  blpnf  13159  xmeter  13195  bdxmet  13260  metrest  13265  xmetxp  13266  metcn  13273  cncffvrn  13328  reefiso  13457