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  437  mpbiran2d  438  bianabs  600  imordc  882  3anibar  1149  xor2dc  1368  bilukdc  1374  reuhypd  4392  opelresi  4830  iota1  5102  funbrfv2b  5466  dffn5im  5467  fneqeql  5528  f1ompt  5571  dff13  5669  fliftcnv  5696  isotr  5717  isoini  5719  caovord3  5944  releldm2  6083  tpostpos  6161  nnsssuc  6398  nnaordi  6404  iserd  6455  ecdmn0m  6471  qliftel  6509  qliftfun  6511  qliftf  6514  ecopovsym  6525  mapen  6740  supisolem  6895  cnvti  6906  omp1eomlem  6979  ctssdc  6998  isomnimap  7009  ismkvmap  7028  recmulnqg  7199  nqtri3or  7204  ltmnqg  7209  mullocprlem  7378  addextpr  7429  gt0srpr  7556  ltsosr  7572  ltasrg  7578  map2psrprg  7613  xrlenlt  7829  letri3  7845  subadd  7965  ltsubadd2  8195  lesubadd2  8197  suble  8202  ltsub23  8204  ltaddpos2  8215  ltsubpos  8216  subge02  8240  ltaddsublt  8333  reapneg  8359  apsym  8368  apti  8384  leltap  8387  ap0gt0  8402  divmulap  8435  divmulap3  8437  rec11rap  8471  ltdiv1  8626  ltdivmul2  8636  ledivmul2  8638  ltrec  8641  suprleubex  8712  nnle1eq1  8744  avgle1  8960  avgle2  8961  nn0le0eq0  9005  znnnlt1  9102  zleltp1  9109  elz2  9122  uzm1  9356  uzin  9358  difrp  9480  xrletri3  9588  xgepnf  9599  xltnegi  9618  xltadd1  9659  xposdif  9665  xleaddadd  9670  elioo5  9716  elfz5  9798  fzdifsuc  9861  elfzm11  9871  uzsplit  9872  elfzonelfzo  10007  qtri3or  10020  qavgle  10036  flqbi  10063  flqbi2  10064  zmodid2  10125  q2submod  10158  sqap0  10359  lt2sq  10366  le2sq  10367  nn0opthlem1d  10466  bcval5  10509  zfz1isolemiso  10582  shftfib  10595  mulreap  10636  caucvgrelemcau  10752  caucvgre  10753  elicc4abs  10866  abs2difabs  10880  cau4  10888  maxclpr  10994  negfi  10999  lemininf  11005  mul0inf  11012  xrlemininf  11040  xrminltinf  11041  clim2  11052  climeq  11068  fisumss  11161  fsumabs  11234  isumshft  11259  absefib  11477  dvdsval3  11497  dvdslelemd  11541  dvdsabseq  11545  dvdsflip  11549  dvdsssfz1  11550  zeo3  11565  ndvdsadd  11628  dvdssq  11719  algcvgblem  11730  lcmdvds  11760  ncoprmgcdgt1b  11771  isprm3  11799  phiprmpw  11898  discld  12305  isneip  12315  restopnb  12350  restopn2  12352  restdis  12353  lmbr2  12383  cnptoprest  12408  cnptoprest2  12409  tx1cn  12438  tx2cn  12439  txcnmpt  12442  txrest  12445  elbl2ps  12561  elbl2  12562  blcomps  12565  blcom  12566  xblpnfps  12567  xblpnf  12568  blpnf  12569  xmeter  12605  bdxmet  12670  metrest  12675  xmetxp  12676  metcn  12683  cncffvrn  12738