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  615  imordc  905  ifpnst  997  3anibar  1192  xor2dc  1435  bilukdc  1441  snelpwg  4331  prelpw  4334  reuhypd  4597  opelresi  5054  iota1  5332  funbrfv2b  5726  dffn5im  5727  fneqeql  5791  f1ompt  5833  dff13  5947  fliftcnv  5974  isotr  5995  isoini  5997  caovord3  6236  releldm2  6392  tpostpos  6508  nnsssuc  6748  nnaordi  6754  iserd  6806  ecdmn0m  6824  qliftel  6862  qliftfun  6864  qliftf  6867  ecopovsym  6878  pw2f1odclem  7100  mapen  7112  suppeqfsuppbi  7261  supisolem  7312  cnvti  7323  omp1eomlem  7398  ctssdc  7417  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  netap  7584  2omotaplemap  7587  recmulnqg  7722  nqtri3or  7727  ltmnqg  7732  mullocprlem  7901  addextpr  7952  gt0srpr  8079  ltsosr  8095  ltasrg  8101  map2psrprg  8136  xrlenlt  8354  letri3  8370  subadd  8492  ltsubadd2  8724  lesubadd2  8726  suble  8731  ltsub23  8733  ltaddpos2  8744  ltsubpos  8745  subge02  8769  ltaddsublt  8862  reapneg  8888  apsym  8897  apti  8913  leltap  8916  ap0gt0  8931  divmulap  8966  divmulap3  8968  rec11rap  9002  ltdiv1  9159  ltdivmul2  9169  ledivmul2  9171  ltrec  9174  suprleubex  9245  nnle1eq1  9278  avgle1  9496  avgle2  9497  nn0le0eq0  9541  znnnlt1  9642  zleltp1  9650  elz2  9666  uzm1  9903  uzin  9905  difrp  10043  xrletri3  10156  xgepnf  10168  xltnegi  10187  xltadd1  10228  xposdif  10234  xleaddadd  10239  elioo5  10285  elfz5  10370  fzdifsuc  10437  elfzm11  10447  uzsplit  10448  elfzonelfzo  10597  qtri3or  10624  qavgle  10642  flqbi  10674  flqbi2  10675  fldiv4lem1div2uz2  10690  zmodid2  10738  q2submod  10771  sqap0  10992  lt2sq  10999  le2sq  11000  nn0opthlem1d  11107  bcval5  11150  zfz1isolemiso  11236  pfxsuffeqwrdeq  11415  shftfib  11533  mulreap  11574  caucvgrelemcau  11690  caucvgre  11691  elicc4abs  11804  abs2difabs  11818  cau4  11826  maxclpr  11932  negfi  11938  lemininf  11944  mul0inf  11951  xrlemininf  11981  xrminltinf  11982  clim2  11993  climeq  12009  fisumss  12103  fsumabs  12176  isumshft  12201  absefib  12482  dvdsval3  12502  dvdslelemd  12554  dvdsabseq  12558  dvdsflip  12562  dvdsssfz1  12563  zeo3  12579  ndvdsadd  12642  bitscmp  12669  dvdssq  12752  algcvgblem  12771  lcmdvds  12801  ncoprmgcdgt1b  12812  isprm3  12840  phiprmpw  12944  prmdiv  12957  pc11  13054  pcz  13055  pockthlem  13079  1arith  13090  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilemsima  13203  ballotfilemfrcn0  13217  ercpbllemg  13627  grpinvcnv  13865  eqger  14025  ablsubadd  14113  dvdsr02  14335  opprunitd  14340  unitsubm  14349  issubrg3  14478  aprval  14514  opprdrng  14543  rnglidlmmgm  14756  znleval2  14914  discld  15113  isneip  15123  restopnb  15158  restopn2  15160  restdis  15161  lmbr2  15191  cnptoprest  15216  cnptoprest2  15217  tx1cn  15246  tx2cn  15247  txcnmpt  15250  txrest  15253  elbl2ps  15369  elbl2  15370  blcomps  15373  blcom  15374  xblpnfps  15375  xblpnf  15376  blpnf  15377  xmeter  15413  bdxmet  15478  metrest  15483  xmetxp  15484  metcn  15491  cncfcdm  15559  reefiso  15754  gausslemma2dlem0c  16036  lgseisenlem3  16057  lgsquadlem1  16062  m1lgs  16070  2lgsoddprmlem2  16091  ausgrusgrben  16275  eupth2lemsfi  16585