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  899  3anibar  1168  xor2dc  1410  bilukdc  1416  reuhypd  4522  opelresi  4975  iota1  5251  funbrfv2b  5630  dffn5im  5631  fneqeql  5695  f1ompt  5738  dff13  5844  fliftcnv  5871  isotr  5892  isoini  5894  caovord3  6127  releldm2  6278  tpostpos  6357  nnsssuc  6595  nnaordi  6601  iserd  6653  ecdmn0m  6671  qliftel  6709  qliftfun  6711  qliftf  6714  ecopovsym  6725  pw2f1odclem  6938  mapen  6950  supisolem  7117  cnvti  7128  omp1eomlem  7203  ctssdc  7222  isomnimap  7246  ismkvmap  7263  iswomnimap  7275  netap  7373  2omotaplemap  7376  recmulnqg  7511  nqtri3or  7516  ltmnqg  7521  mullocprlem  7690  addextpr  7741  gt0srpr  7868  ltsosr  7884  ltasrg  7890  map2psrprg  7925  xrlenlt  8144  letri3  8160  subadd  8282  ltsubadd2  8513  lesubadd2  8515  suble  8520  ltsub23  8522  ltaddpos2  8533  ltsubpos  8534  subge02  8558  ltaddsublt  8651  reapneg  8677  apsym  8686  apti  8702  leltap  8705  ap0gt0  8720  divmulap  8755  divmulap3  8757  rec11rap  8791  ltdiv1  8948  ltdivmul2  8958  ledivmul2  8960  ltrec  8963  suprleubex  9034  nnle1eq1  9067  avgle1  9285  avgle2  9286  nn0le0eq0  9330  znnnlt1  9427  zleltp1  9435  elz2  9451  uzm1  9686  uzin  9688  difrp  9821  xrletri3  9933  xgepnf  9945  xltnegi  9964  xltadd1  10005  xposdif  10011  xleaddadd  10016  elioo5  10062  elfz5  10146  fzdifsuc  10210  elfzm11  10220  uzsplit  10221  elfzonelfzo  10366  qtri3or  10390  qavgle  10408  flqbi  10440  flqbi2  10441  fldiv4lem1div2uz2  10456  zmodid2  10504  q2submod  10537  sqap0  10758  lt2sq  10765  le2sq  10766  nn0opthlem1d  10872  bcval5  10915  zfz1isolemiso  10991  pfxsuffeqwrdeq  11157  shftfib  11178  mulreap  11219  caucvgrelemcau  11335  caucvgre  11336  elicc4abs  11449  abs2difabs  11463  cau4  11471  maxclpr  11577  negfi  11583  lemininf  11589  mul0inf  11596  xrlemininf  11626  xrminltinf  11627  clim2  11638  climeq  11654  fisumss  11747  fsumabs  11820  isumshft  11845  absefib  12126  dvdsval3  12146  dvdslelemd  12198  dvdsabseq  12202  dvdsflip  12206  dvdsssfz1  12207  zeo3  12223  ndvdsadd  12286  bitscmp  12313  dvdssq  12396  algcvgblem  12415  lcmdvds  12445  ncoprmgcdgt1b  12456  isprm3  12484  phiprmpw  12588  prmdiv  12601  pc11  12698  pcz  12699  pockthlem  12723  1arith  12734  ercpbllemg  13206  grpinvcnv  13444  eqger  13604  ablsubadd  13692  dvdsr02  13911  opprunitd  13916  unitsubm  13925  issubrg3  14053  aprval  14088  rnglidlmmgm  14302  znleval2  14460  discld  14652  isneip  14662  restopnb  14697  restopn2  14699  restdis  14700  lmbr2  14730  cnptoprest  14755  cnptoprest2  14756  tx1cn  14785  tx2cn  14786  txcnmpt  14789  txrest  14792  elbl2ps  14908  elbl2  14909  blcomps  14912  blcom  14913  xblpnfps  14914  xblpnf  14915  blpnf  14916  xmeter  14952  bdxmet  15017  metrest  15022  xmetxp  15023  metcn  15030  cncfcdm  15098  reefiso  15293  gausslemma2dlem0c  15572  lgseisenlem3  15593  lgsquadlem1  15598  m1lgs  15606  2lgsoddprmlem2  15627