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  4507  opelresi  4958  iota1  5234  funbrfv2b  5608  dffn5im  5609  fneqeql  5673  f1ompt  5716  dff13  5818  fliftcnv  5845  isotr  5866  isoini  5868  caovord3  6101  releldm2  6252  tpostpos  6331  nnsssuc  6569  nnaordi  6575  iserd  6627  ecdmn0m  6645  qliftel  6683  qliftfun  6685  qliftf  6688  ecopovsym  6699  pw2f1odclem  6904  mapen  6916  supisolem  7083  cnvti  7094  omp1eomlem  7169  ctssdc  7188  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  netap  7337  2omotaplemap  7340  recmulnqg  7475  nqtri3or  7480  ltmnqg  7485  mullocprlem  7654  addextpr  7705  gt0srpr  7832  ltsosr  7848  ltasrg  7854  map2psrprg  7889  xrlenlt  8108  letri3  8124  subadd  8246  ltsubadd2  8477  lesubadd2  8479  suble  8484  ltsub23  8486  ltaddpos2  8497  ltsubpos  8498  subge02  8522  ltaddsublt  8615  reapneg  8641  apsym  8650  apti  8666  leltap  8669  ap0gt0  8684  divmulap  8719  divmulap3  8721  rec11rap  8755  ltdiv1  8912  ltdivmul2  8922  ledivmul2  8924  ltrec  8927  suprleubex  8998  nnle1eq1  9031  avgle1  9249  avgle2  9250  nn0le0eq0  9294  znnnlt1  9391  zleltp1  9398  elz2  9414  uzm1  9649  uzin  9651  difrp  9784  xrletri3  9896  xgepnf  9908  xltnegi  9927  xltadd1  9968  xposdif  9974  xleaddadd  9979  elioo5  10025  elfz5  10109  fzdifsuc  10173  elfzm11  10183  uzsplit  10184  elfzonelfzo  10323  qtri3or  10347  qavgle  10365  flqbi  10397  flqbi2  10398  fldiv4lem1div2uz2  10413  zmodid2  10461  q2submod  10494  sqap0  10715  lt2sq  10722  le2sq  10723  nn0opthlem1d  10829  bcval5  10872  zfz1isolemiso  10948  shftfib  11005  mulreap  11046  caucvgrelemcau  11162  caucvgre  11163  elicc4abs  11276  abs2difabs  11290  cau4  11298  maxclpr  11404  negfi  11410  lemininf  11416  mul0inf  11423  xrlemininf  11453  xrminltinf  11454  clim2  11465  climeq  11481  fisumss  11574  fsumabs  11647  isumshft  11672  absefib  11953  dvdsval3  11973  dvdslelemd  12025  dvdsabseq  12029  dvdsflip  12033  dvdsssfz1  12034  zeo3  12050  ndvdsadd  12113  bitscmp  12140  dvdssq  12223  algcvgblem  12242  lcmdvds  12272  ncoprmgcdgt1b  12283  isprm3  12311  phiprmpw  12415  prmdiv  12428  pc11  12525  pcz  12526  pockthlem  12550  1arith  12561  ercpbllemg  13032  grpinvcnv  13270  eqger  13430  ablsubadd  13518  dvdsr02  13737  opprunitd  13742  unitsubm  13751  issubrg3  13879  aprval  13914  rnglidlmmgm  14128  znleval2  14286  discld  14456  isneip  14466  restopnb  14501  restopn2  14503  restdis  14504  lmbr2  14534  cnptoprest  14559  cnptoprest2  14560  tx1cn  14589  tx2cn  14590  txcnmpt  14593  txrest  14596  elbl2ps  14712  elbl2  14713  blcomps  14716  blcom  14717  xblpnfps  14718  xblpnf  14719  blpnf  14720  xmeter  14756  bdxmet  14821  metrest  14826  xmetxp  14827  metcn  14834  cncfcdm  14902  reefiso  15097  gausslemma2dlem0c  15376  lgseisenlem3  15397  lgsquadlem1  15402  m1lgs  15410  2lgsoddprmlem2  15431