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  4486  opelresi  4933  iota1  5207  funbrfv2b  5577  dffn5im  5578  fneqeql  5641  f1ompt  5684  dff13  5786  fliftcnv  5813  isotr  5834  isoini  5836  caovord3  6066  releldm2  6205  tpostpos  6284  nnsssuc  6522  nnaordi  6528  iserd  6580  ecdmn0m  6596  qliftel  6634  qliftfun  6636  qliftf  6639  ecopovsym  6650  mapen  6865  supisolem  7027  cnvti  7038  omp1eomlem  7113  ctssdc  7132  isomnimap  7155  ismkvmap  7172  iswomnimap  7184  netap  7273  2omotaplemap  7276  recmulnqg  7410  nqtri3or  7415  ltmnqg  7420  mullocprlem  7589  addextpr  7640  gt0srpr  7767  ltsosr  7783  ltasrg  7789  map2psrprg  7824  xrlenlt  8042  letri3  8058  subadd  8180  ltsubadd2  8410  lesubadd2  8412  suble  8417  ltsub23  8419  ltaddpos2  8430  ltsubpos  8431  subge02  8455  ltaddsublt  8548  reapneg  8574  apsym  8583  apti  8599  leltap  8602  ap0gt0  8617  divmulap  8652  divmulap3  8654  rec11rap  8688  ltdiv1  8845  ltdivmul2  8855  ledivmul2  8857  ltrec  8860  suprleubex  8931  nnle1eq1  8963  avgle1  9179  avgle2  9180  nn0le0eq0  9224  znnnlt1  9321  zleltp1  9328  elz2  9344  uzm1  9578  uzin  9580  difrp  9712  xrletri3  9824  xgepnf  9836  xltnegi  9855  xltadd1  9896  xposdif  9902  xleaddadd  9907  elioo5  9953  elfz5  10037  fzdifsuc  10101  elfzm11  10111  uzsplit  10112  elfzonelfzo  10250  qtri3or  10263  qavgle  10279  flqbi  10310  flqbi2  10311  zmodid2  10372  q2submod  10405  sqap0  10607  lt2sq  10614  le2sq  10615  nn0opthlem1d  10720  bcval5  10763  zfz1isolemiso  10839  shftfib  10852  mulreap  10893  caucvgrelemcau  11009  caucvgre  11010  elicc4abs  11123  abs2difabs  11137  cau4  11145  maxclpr  11251  negfi  11256  lemininf  11262  mul0inf  11269  xrlemininf  11299  xrminltinf  11300  clim2  11311  climeq  11327  fisumss  11420  fsumabs  11493  isumshft  11518  absefib  11798  dvdsval3  11818  dvdslelemd  11869  dvdsabseq  11873  dvdsflip  11877  dvdsssfz1  11878  zeo3  11893  ndvdsadd  11956  dvdssq  12052  algcvgblem  12069  lcmdvds  12099  ncoprmgcdgt1b  12110  isprm3  12138  phiprmpw  12242  prmdiv  12255  pc11  12350  pcz  12351  pockthlem  12374  1arith  12385  ercpbllemg  12779  grpinvcnv  12985  eqger  13136  ablsubadd  13219  dvdsr02  13423  opprunitd  13428  unitsubm  13437  issubrg3  13562  aprval  13566  rnglidlmmgm  13780  discld  14040  isneip  14050  restopnb  14085  restopn2  14087  restdis  14088  lmbr2  14118  cnptoprest  14143  cnptoprest2  14144  tx1cn  14173  tx2cn  14174  txcnmpt  14177  txrest  14180  elbl2ps  14296  elbl2  14297  blcomps  14300  blcom  14301  xblpnfps  14302  xblpnf  14303  blpnf  14304  xmeter  14340  bdxmet  14405  metrest  14410  xmetxp  14411  metcn  14418  cncfcdm  14473  reefiso  14602  m1lgs  14856  2lgsoddprmlem2  14858