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  4502  opelresi  4953  iota1  5229  funbrfv2b  5601  dffn5im  5602  fneqeql  5666  f1ompt  5709  dff13  5811  fliftcnv  5838  isotr  5859  isoini  5861  caovord3  6092  releldm2  6238  tpostpos  6317  nnsssuc  6555  nnaordi  6561  iserd  6613  ecdmn0m  6631  qliftel  6669  qliftfun  6671  qliftf  6674  ecopovsym  6685  pw2f1odclem  6890  mapen  6902  supisolem  7067  cnvti  7078  omp1eomlem  7153  ctssdc  7172  isomnimap  7196  ismkvmap  7213  iswomnimap  7225  netap  7314  2omotaplemap  7317  recmulnqg  7451  nqtri3or  7456  ltmnqg  7461  mullocprlem  7630  addextpr  7681  gt0srpr  7808  ltsosr  7824  ltasrg  7830  map2psrprg  7865  xrlenlt  8084  letri3  8100  subadd  8222  ltsubadd2  8452  lesubadd2  8454  suble  8459  ltsub23  8461  ltaddpos2  8472  ltsubpos  8473  subge02  8497  ltaddsublt  8590  reapneg  8616  apsym  8625  apti  8641  leltap  8644  ap0gt0  8659  divmulap  8694  divmulap3  8696  rec11rap  8730  ltdiv1  8887  ltdivmul2  8897  ledivmul2  8899  ltrec  8902  suprleubex  8973  nnle1eq1  9006  avgle1  9223  avgle2  9224  nn0le0eq0  9268  znnnlt1  9365  zleltp1  9372  elz2  9388  uzm1  9623  uzin  9625  difrp  9758  xrletri3  9870  xgepnf  9882  xltnegi  9901  xltadd1  9942  xposdif  9948  xleaddadd  9953  elioo5  9999  elfz5  10083  fzdifsuc  10147  elfzm11  10157  uzsplit  10158  elfzonelfzo  10297  qtri3or  10310  qavgle  10327  flqbi  10359  flqbi2  10360  fldiv4lem1div2uz2  10375  zmodid2  10423  q2submod  10456  sqap0  10677  lt2sq  10684  le2sq  10685  nn0opthlem1d  10791  bcval5  10834  zfz1isolemiso  10910  shftfib  10967  mulreap  11008  caucvgrelemcau  11124  caucvgre  11125  elicc4abs  11238  abs2difabs  11252  cau4  11260  maxclpr  11366  negfi  11371  lemininf  11377  mul0inf  11384  xrlemininf  11414  xrminltinf  11415  clim2  11426  climeq  11442  fisumss  11535  fsumabs  11608  isumshft  11633  absefib  11914  dvdsval3  11934  dvdslelemd  11985  dvdsabseq  11989  dvdsflip  11993  dvdsssfz1  11994  zeo3  12009  ndvdsadd  12072  dvdssq  12168  algcvgblem  12187  lcmdvds  12217  ncoprmgcdgt1b  12228  isprm3  12256  phiprmpw  12360  prmdiv  12373  pc11  12469  pcz  12470  pockthlem  12494  1arith  12505  ercpbllemg  12913  grpinvcnv  13140  eqger  13294  ablsubadd  13382  dvdsr02  13601  opprunitd  13606  unitsubm  13615  issubrg3  13743  aprval  13778  rnglidlmmgm  13992  znleval2  14142  discld  14304  isneip  14314  restopnb  14349  restopn2  14351  restdis  14352  lmbr2  14382  cnptoprest  14407  cnptoprest2  14408  tx1cn  14437  tx2cn  14438  txcnmpt  14441  txrest  14444  elbl2ps  14560  elbl2  14561  blcomps  14564  blcom  14565  xblpnfps  14566  xblpnf  14567  blpnf  14568  xmeter  14604  bdxmet  14669  metrest  14674  xmetxp  14675  metcn  14682  cncfcdm  14737  reefiso  14912  gausslemma2dlem0c  15167  lgseisenlem3  15188  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem2  15194