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  7348  cnvti  7359  omp1eomlem  7434  ctssdc  7453  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  netap  7620  2omotaplemap  7623  recmulnqg  7758  nqtri3or  7763  ltmnqg  7768  mullocprlem  7937  addextpr  7988  gt0srpr  8115  ltsosr  8131  ltasrg  8137  map2psrprg  8172  xrlenlt  8390  letri3  8406  subadd  8529  ltsubadd2  8761  lesubadd2  8763  suble  8768  ltsub23  8770  ltaddpos2  8781  ltsubpos  8782  subge02  8806  ltaddsublt  8900  reapneg  8926  apsym  8935  apti  8951  leltap  8954  ap0gt0  8969  divmulap  9006  divmulap3  9008  rec11rap  9042  ltdiv1  9199  ltdivmul2  9209  ledivmul2  9211  ltrec  9214  suprleubex  9285  nnle1eq1  9329  avgle1  9548  avgle2  9549  nn0le0eq0  9593  znnnlt1  9694  zleltp1  9702  elz2  9718  uzm1  9955  uzin  9957  difrp  10095  xrletri3  10208  xgepnf  10220  xltnegi  10239  xltadd1  10280  xposdif  10286  xleaddadd  10291  elioo5  10337  elfz5  10422  fzdifsuc  10490  elfzm11  10500  uzsplit  10501  elfzonelfzo  10650  qtri3or  10677  qavgle  10695  flqbi  10727  flqbi2  10728  fldiv4lem1div2uz2  10743  zmodid2  10791  q2submod  10824  sqap0  11045  lt2sq  11052  le2sq  11053  nn0opthlem1d  11160  bcval5  11203  zfz1isolemiso  11293  pfxsuffeqwrdeq  11472  shftfib  11590  mulreap  11631  caucvgrelemcau  11748  caucvgre  11749  elicc4abs  11862  abs2difabs  11876  cau4  11884  maxclpr  11990  negfi  11996  lemininf  12002  mul0inf  12009  xrlemininf  12039  xrminltinf  12040  clim2  12051  climeq  12067  fisumss  12161  fsumabs  12234  isumshft  12259  absefib  12540  dvdsval3  12560  dvdslelemd  12612  dvdsabseq  12616  dvdsflip  12620  dvdsssfz1  12621  zeo3  12637  ndvdsadd  12700  bitscmp  12727  dvdssq  12810  algcvgblem  12829  lcmdvds  12859  ncoprmgcdgt1b  12870  isprm3  12898  phiprmpw  13002  prmdiv  13015  pc11  13112  pcz  13113  pockthlem  13137  1arith  13148  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemodife  13242  ballotfilemsima  13261  ballotfilemfrcn0  13275  ercpbllemg  13653  grpinvcnv  13875  eqger  14029  ablsubadd  14118  dvdsr02  14414  opprunitd  14419  unitsubm  14428  issubrg3  14557  aprval  14593  opprdrng  14622  rnglidlmmgm  14835  znleval2  14991  discld  15239  isneip  15249  restopnb  15284  restopn2  15286  restdis  15287  lmbr2  15317  cnptoprest  15342  cnptoprest2  15343  tx1cn  15372  tx2cn  15373  txcnmpt  15376  txrest  15379  elbl2ps  15495  elbl2  15496  blcomps  15499  blcom  15500  xblpnfps  15501  xblpnf  15502  blpnf  15503  xmeter  15539  bdxmet  15604  metrest  15609  xmetxp  15610  metcn  15617  cncfcdm  15685  reefiso  15880  bclbnd  16127  gausslemma2dlem0c  16182  lgseisenlem3  16203  lgsquadlem1  16208  m1lgs  16216  2lgsoddprmlem2  16237  ausgrusgrben  16421  eupth2lemsfi  16731