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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr2d  216  3bitr2rd  217  3bitr4d  220  3bitr4rd  221  mpbirand  445  mpbiran2d  446  bianabs  619  imordc  909  ifpnst  1001  3anibar  1196  xor2dc  1439  bilukdc  1445  snelpwg  4352  prelpw  4355  reuhypd  4619  opelresi  5076  iota1  5355  funbrfv2b  5750  dffn5im  5751  fneqeql  5820  f1ompt  5862  dff13  5977  fliftcnv  6004  isotr  6025  isoini  6027  caovord3  6266  releldm2  6423  tpostpos  6539  nnsssuc  6779  nnaordi  6785  iserd  6837  ecdmn0m  6855  qliftel  6893  qliftfun  6895  qliftf  6898  ecopovsym  6909  pw2f1odclem  7139  mapen  7151  relresfin  7269  suppeqfsuppbi  7301  supisolem  7355  cnvti  7366  omp1eomlem  7441  ctssdc  7460  isomnimap  7484  ismkvmap  7501  iswomnimap  7513  netap  7627  2omotaplemap  7630  recmulnqg  7765  nqtri3or  7770  ltmnqg  7775  mullocprlem  7944  addextpr  7995  gt0srpr  8122  ltsosr  8138  ltasrg  8144  map2psrprg  8179  xrlenlt  8397  letri3  8413  subadd  8537  ltsubadd2  8769  lesubadd2  8771  suble  8776  ltsub23  8778  ltaddpos2  8789  ltsubpos  8790  subge02  8814  ltaddsublt  8908  reapneg  8934  apsym  8943  apti  8959  leltap  8962  ap0gt0  8977  divmulap  9014  divmulap3  9016  rec11rap  9050  ltdiv1  9207  ltdivmul2  9217  ledivmul2  9219  ltrec  9222  suprleubex  9293  nnle1eq1  9338  avgle1  9558  avgle2  9559  nn0le0eq0  9603  znnnlt1  9704  zleltp1  9712  elz2  9728  uzm1  9970  uzin  9972  difrp  10111  xrletri3  10224  xgepnf  10236  xltnegi  10255  xltadd1  10296  xposdif  10302  xleaddadd  10307  elioo5  10353  elfz5  10438  fzdifsuc  10506  elfzm11  10516  uzsplit  10517  elfzonelfzo  10666  qtri3or  10693  qavgle  10711  flqbi  10747  flqbi2  10748  fldiv4lem1div2uz2  10763  zmodid2  10811  q2submod  10844  sqap0  11065  lt2sq  11072  le2sq  11073  nn0opthlem1d  11181  bcval5  11224  zfz1isolemiso  11314  pfxsuffeqwrdeq  11493  shftfib  11611  mulreap  11652  caucvgrelemcau  11769  caucvgre  11770  elicc4abs  11884  abs2difabs  11898  cau4  11906  maxclpr  12012  negfi  12018  lemininf  12025  mul0inf  12033  xrlemininf  12063  xrminltinf  12064  clim2  12075  climeq  12091  fisumss  12185  fsumabs  12258  isumshft  12283  absefib  12564  dvdsval3  12584  dvdslelemd  12636  dvdsabseq  12640  dvdsflip  12644  dvdsssfz1  12645  zeo3  12661  ndvdsadd  12724  bitscmp  12751  dvdssq  12834  algcvgblem  12853  lcmdvds  12883  ncoprmgcdgt1b  12894  isprm3  12922  phiprmpw  13030  prmdiv  13043  pc11  13140  pcz  13141  pockthlem  13165  1arith  13176  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemodife  13299  ballotfilemsima  13318  ballotfilemfrcn0  13332  ercpbllemg  13711  grpinvcnv  13933  eqger  14087  ablsubadd  14207  dvdsr02  14522  opprunitd  14527  unitsubm  14536  issubrg3  14665  aprval  14701  opprdrng  14730  rnglidlmmgm  14943  znleval2  15099  discld  15374  isneip  15384  restopnb  15419  restopn2  15421  restdis  15422  lmbr2  15452  cnptoprest  15477  cnptoprest2  15478  tx1cn  15507  tx2cn  15508  txcnmpt  15511  txrest  15514  elbl2ps  15630  elbl2  15631  blcomps  15634  blcom  15635  xblpnfps  15636  xblpnf  15637  blpnf  15638  xmeter  15674  bdxmet  15739  metrest  15744  xmetxp  15745  metcn  15752  cncfcdm  15820  reefiso  16015  bclbnd  16319  bposlem1  16323  bposlem5  16327  bpos  16332  gausslemma2dlem0c  16387  lgseisenlem3  16408  lgsquadlem1  16413  m1lgs  16421  2lgsoddprmlem2  16442  ausgrusgrben  16626  eupth2lemsfi  16936