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  4350  prelpw  4353  reuhypd  4617  opelresi  5074  iota1  5352  funbrfv2b  5747  dffn5im  5748  fneqeql  5817  f1ompt  5859  dff13  5974  fliftcnv  6001  isotr  6022  isoini  6024  caovord3  6263  releldm2  6419  tpostpos  6535  nnsssuc  6775  nnaordi  6781  iserd  6833  ecdmn0m  6851  qliftel  6889  qliftfun  6891  qliftf  6894  ecopovsym  6905  pw2f1odclem  7134  mapen  7146  suppeqfsuppbi  7295  supisolem  7349  cnvti  7360  omp1eomlem  7435  ctssdc  7454  isomnimap  7478  ismkvmap  7495  iswomnimap  7507  netap  7621  2omotaplemap  7624  recmulnqg  7759  nqtri3or  7764  ltmnqg  7769  mullocprlem  7938  addextpr  7989  gt0srpr  8116  ltsosr  8132  ltasrg  8138  map2psrprg  8173  xrlenlt  8391  letri3  8407  subadd  8531  ltsubadd2  8763  lesubadd2  8765  suble  8770  ltsub23  8772  ltaddpos2  8783  ltsubpos  8784  subge02  8808  ltaddsublt  8902  reapneg  8928  apsym  8937  apti  8953  leltap  8956  ap0gt0  8971  divmulap  9008  divmulap3  9010  rec11rap  9044  ltdiv1  9201  ltdivmul2  9211  ledivmul2  9213  ltrec  9216  suprleubex  9287  nnle1eq1  9331  avgle1  9551  avgle2  9552  nn0le0eq0  9596  znnnlt1  9697  zleltp1  9705  elz2  9721  uzm1  9963  uzin  9965  difrp  10104  xrletri3  10217  xgepnf  10229  xltnegi  10248  xltadd1  10289  xposdif  10295  xleaddadd  10300  elioo5  10346  elfz5  10431  fzdifsuc  10499  elfzm11  10509  uzsplit  10510  elfzonelfzo  10659  qtri3or  10686  qavgle  10704  flqbi  10739  flqbi2  10740  fldiv4lem1div2uz2  10755  zmodid2  10803  q2submod  10836  sqap0  11057  lt2sq  11064  le2sq  11065  nn0opthlem1d  11173  bcval5  11216  zfz1isolemiso  11306  pfxsuffeqwrdeq  11485  shftfib  11603  mulreap  11644  caucvgrelemcau  11761  caucvgre  11762  elicc4abs  11876  abs2difabs  11890  cau4  11898  maxclpr  12004  negfi  12010  lemininf  12017  mul0inf  12025  xrlemininf  12055  xrminltinf  12056  clim2  12067  climeq  12083  fisumss  12177  fsumabs  12250  isumshft  12275  absefib  12556  dvdsval3  12576  dvdslelemd  12628  dvdsabseq  12632  dvdsflip  12636  dvdsssfz1  12637  zeo3  12653  ndvdsadd  12716  bitscmp  12743  dvdssq  12826  algcvgblem  12845  lcmdvds  12875  ncoprmgcdgt1b  12886  isprm3  12914  phiprmpw  13022  prmdiv  13035  pc11  13132  pcz  13133  pockthlem  13157  1arith  13168  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemodife  13291  ballotfilemsima  13310  ballotfilemfrcn0  13324  ercpbllemg  13702  grpinvcnv  13924  eqger  14078  ablsubadd  14167  dvdsr02  14463  opprunitd  14468  unitsubm  14477  issubrg3  14606  aprval  14642  opprdrng  14671  rnglidlmmgm  14884  znleval2  15040  discld  15289  isneip  15299  restopnb  15334  restopn2  15336  restdis  15337  lmbr2  15367  cnptoprest  15392  cnptoprest2  15393  tx1cn  15422  tx2cn  15423  txcnmpt  15426  txrest  15429  elbl2ps  15545  elbl2  15546  blcomps  15549  blcom  15550  xblpnfps  15551  xblpnf  15552  blpnf  15553  xmeter  15589  bdxmet  15654  metrest  15659  xmetxp  15660  metcn  15667  cncfcdm  15735  reefiso  15930  bclbnd  16229  bposlem1  16233  bposlem5  16237  gausslemma2dlem0c  16292  lgseisenlem3  16313  lgsquadlem1  16318  m1lgs  16326  2lgsoddprmlem2  16347  ausgrusgrben  16531  eupth2lemsfi  16841