Theorem bitrd 188

Description: Deduction form of bitri 184. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)

Hypotheses

Ref	Expression
bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	pm5.74i 180	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3		bitrd.2	. . . 4 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	3	pm5.74i 180	. . 3 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃))
5	2, 4	bitri 184	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜃))
6	5	pm5.74ri 181	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:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  466  anbi12d  477  orbi12d  805  con1biidc  889  pm4.54dc  914  dn1dc  973  dedlem0a  981  dfifp3dc  995  dfifp4dc  996  dfifp5dc  997  3bior2fd  1395  xorbi12d  1431  nbbndc  1443  eleq12d  2309  neeq12d  2440  neleq12d  2521  raleqbi1dv  2761  rexeqbi1dv  2762  reueqd  2763  rmoeqd  2764  raleqbidv  2765  rexeqbidv  2766  raleqbidva  2767  rexeqbidva  2768  eueq3dc  3000  sbc19.21g  3120  sbcabel  3134  sbcel1g  3166  sbceq1g  3167  sbcel2g  3168  sbceq2g  3169  sbccsb2g  3177  sbcco3g  3205  sseq12d  3279  raaanlem  3632  sbcssg  3636  ralsng  3749  2ralunsn  3924  csbunig  3943  disjeq12d  4115  breq123d  4144  sbcbr12g  4186  sbcbr1g  4187  sbcbr2g  4188  treq  4235  nalset  4263  exmidsssn  4339  copsex4g  4387  onsucb  4650  posng  4847  csbxpg  4856  sbcrel  4861  csbcnvg  4964  eliniseg  5157  brcodir  5175  csbrng  5249  sbcfung  5401  fneq12d  5473  feq12d  5523  feq123d  5524  sbcfng  5531  sbcfg  5532  f1osng  5682  csbfv12g  5736  funimass4  5753  dmfco  5773  eqfnfv  5806  eqfnfv2  5807  fneqeql2  5818  fvimacnvi  5823  funimass3  5825  fniniseg  5829  unpreima  5833  ralrnmpt  5850  rexrnmpt  5851  dffo3  5855  fmptco  5874  fressnfv  5902  eufnfv  5949  foima2  5957  fnunirn  5973  dff13  5974  f1elima  5979  cocan1  5993  cocan2  5994  fliftel  5999  fliftf  6005  isoresbr  6015  isoini  6024  f1oiso  6032  f1ofveu  6073  mpoeq123dva  6149  ovid  6205  ov  6208  ovg  6228  ovelrn  6238  caovord2d  6259  ofrfval2  6319  offveqb  6322  eqop  6411  reldm  6420  f1od2  6471  suppval1  6479  suppssrst  6501  suppssrgst  6502  mpoxopoveq  6511  mpoxopovel  6512  tpostpos  6535  smoiso  6573  frecabcl  6670  frecsuclem  6677  nnaordr  6783  nnaword  6784  nnaordex  6801  ereq1  6814  brdifun  6834  erth2  6854  qliftfun  6891  brecop  6899  elmapg  6935  elpmg  6938  mapsnd  6970  dom2lem  7058  xpcomco  7124  pw2f1odclem  7134  php5fin  7186  funisfsupp  7291  ffsuppbi  7300  elfi2  7306  supisolem  7349  inflbti  7365  inl11  7406  ismkvnex  7496  mkvprop  7499  nninfwlporlemd  7513  exmidfodomrlemreseldju  7553  ltapig  7706  ltmpig  7707  nlt1pig  7709  mulcmpblnq  7736  ltsonq  7766  lt2addnq  7772  lt2mulnq  7773  archnqq  7785  prarloclemarch  7786  ltrnqg  7788  mulcmpblnq0  7812  preqlu  7840  genpdflem  7875  addnqprllem  7895  addnqprulem  7896  addlocprlemgt  7902  appdivnq  7931  mulnqprl  7936  mulnqpru  7937  mullocprlem  7938  distrlem4prl  7952  distrlem4pru  7953  1idprl  7958  1idpru  7959  ltexprlemloc  7975  cauappcvgprlemladdrl  8025  cauappcvgprlemladd  8026  cauappcvgprlem1  8027  archrecnq  8031  caucvgprlemnkj  8034  caucvgprprlemexb  8075  addcmpblnr  8107  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1  8149  srpospr  8151  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  map2psrprg  8173  ltresr  8207  axcaucvglemres  8267  eqlelt  8413  cnegexlem1  8503  negeu  8519  subadd2  8532  subcan2  8553  addrsub  8699  ltaddneg  8754  ltaddnegr  8755  ltadd1  8759  leadd2  8761  ltsubadd  8762  lesubadd  8764  ltaddsub2  8767  leaddsub2  8769  ltaddpos  8782  lesub2  8787  ltsub2  8789  ltnegcon1  8793  ltnegcon2  8794  lenegcon1  8796  lenegcon2  8797  addge01  8802  addge02  8803  suble0  8806  leaddle0  8807  lesub0  8809  eqord2  8814  sublt0d  8901  recexre  8909  reaplt  8919  reapltxor  8920  reapneg  8928  remulext1  8930  apreim  8934  apcotr  8938  apadd2  8940  addext  8941  apsub1  8973  mulcanap2d  8993  diveqap0  9015  diveqap1  9038  apmul2  9122  ltmul2  9189  lemul2  9190  ltmulgt11  9197  ltmulgt12  9198  gt0div  9203  ge0div  9204  ltmuldiv  9207  ltrec1  9221  lerec2  9222  ledivdiv  9223  ltdiv23  9225  lediv23  9226  suprleubex  9287  creur  9292  creui  9293  nn1suc  9326  nnrecl  9566  fcdmnn0fsuppg  9623  znnsub  9701  zgt0ge1  9708  zltlen  9729  nn0n0n1ge2b  9730  nn0le2is012  9733  btwnnz  9745  gtndiv  9746  prime  9750  eluz2  9937  indstr2  10019  negm  10025  nn01to3  10027  qapne  10049  qltlen  10050  qreccl  10052  irrmulap  10059  divlt1lt  10136  divle1le  10137  nnledivrp  10178  xnn0xadd0  10280  xltadd2  10290  xsubge0  10294  xlesubadd  10296  iccid  10338  elioc2  10349  elico2  10350  elicc2  10351  elfz2  10429  fzen  10458  fzsubel  10477  elfzp1  10490  fzpr  10495  fzrevral2  10524  fzrevral3  10525  nn0disj  10556  2ffzeq  10559  fzosplitsni  10665  fvinim0ffz  10671  ioo0  10705  ico0  10707  ioc0  10708  modq0  10780  negqmod0  10782  zmodidfzo  10804  frecuzrdgtcl  10863  nn0ennn  10884  nninfinf  10894  sq11  11063  nn0le2msqd  11172  nn0opth2d  11176  hashen  11238  zfz1isolem1  11307  zfz1iso  11308  csbwrdg  11349  wrdnval  11350  eqwrd  11360  ccat0  11379  ccatws1lenp1bg  11418  swrd0g  11447  swrdspsleq  11454  pfxeq  11483  pfxsuffeqwrdeq  11485  pfxsuff1eqwrdeq  11486  ccatopth2  11504  wrd2ind  11510  2shfti  11611  cjap  11687  cnreim  11759  rexfiuz  11770  rexanuz2  11772  abs00ap  11843  absext  11844  sqabs  11864  abslt  11870  absle  11871  absdiflt  11874  absdifle  11875  lenegsq  11877  minmax  12013  ltmininf  12018  mingeb  12026  xrminmax  12049  xrmin1inf  12051  xrmin2inf  12052  xrltmininf  12054  xrlemininf  12055  clim  12065  clim0c  12070  climrecvg1n  12132  zsumdc  12169  fsum2dlemstep  12219  binomlem  12268  pwm1geoserap1  12293  zproddc  12364  efieq  12520  sin01bnd  12542  cos01bnd  12543  dvdsval2  12575  modm1div  12585  zdvdsdc  12597  modmulconst  12608  dvdsaddr  12622  dvdsabseq  12632  fzocongeq  12643  zeo3  12653  odd2np1  12658  oddp1d2  12675  zob  12676  oddm1d2  12677  nnoddm1d2  12695  divalgb  12710  divalgmod  12712  modremain  12714  bits0  12733  bitsp1e  12737  bitsp1o  12738  bitscmp  12743  bitsinv1lem  12746  gcdn0gt0  12773  bezoutlemstep  12792  dvdssq  12826  nn0seqcvgd  12837  algcvgblem  12845  lcmdvds  12875  lcmgcdeq  12879  coprmdvds  12888  qredeq  12892  congr  12896  isprm2  12913  isprm3  12914  prmdvdsexp  12945  prmdvdsexpb  12946  prmexpb  12948  prmfac1  12949  cncongrprm  12954  nnmaxpwlemxy  12966  nnmaxpwlemnfac  12969  qnumdenbi  12990  qnumgt0  12996  hashdvds  13021  crth  13024  fermltl  13034  modprminveq  13051  pcpremul  13094  pc2dvds  13131  pcz  13133  prmpwdvds  13156  4sqlem16  13207  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemodife  13291  ballotfilemrv1  13315  ballotfilemrv2  13316  ballotfilem1ri  13329  oddennn  13334  ctinfomlemom  13369  mgm1  13741  ismhm  13819  mhmpropd  13824  issubm  13830  issubm2  13831  grpsubrcan  13937  grplactcnv  13958  grp1  13962  eqgval  14077  eqgid  14080  quselbasg  14084  isghm  14097  conjnmzb  14134  iscmn  14147  eqgabl  14185  prdsbasmpt  14231  prdsbasmpt2  14239  rngmneg1  14297  rngmneg2  14298  rngpropd  14305  rngen1zr  14311  srgen1zr0  14343  ringideu  14372  ringpropd  14394  crngpropd  14395  dvdsrd  14452  dvdsr02  14463  opprunitd  14468  crngunit  14469  unitpropdg  14506  rhmunitinv  14536  isnzr2  14542  issubrng  14558  resrhm2b  14608  aprval  14642  aprunit  14643  isdrngtap  14657  opprdrng  14671  islmod  14678  islssm  14745  islssmg  14746  ellspsn  14805  isridl  14892  zrhrhmb  15008  zndvds  15035  znleval  15039  isassa  15053  istopg  15152  eltg  15205  eltg2  15206  tgss2  15232  bastop1  15236  bastop2  15237  iscld  15256  isnei  15297  neiint  15298  iscn  15350  iscnp  15352  iscnp3  15356  tgcn  15361  ssidcn  15363  lmbr2  15367  lmbrf  15368  cnnei  15385  cnrest2  15389  eltx  15412  imasnopn  15452  ispsmet  15476  ismet  15497  isxmet  15498  metn0  15531  xmetres2  15532  elbl3ps  15547  elbl3  15548  xblpnfps  15551  xblpnf  15552  elmopn2  15602  metss  15647  bdxmet  15654  metrest  15659  xmetxp  15660  xmetxpbl  15661  metcnp3  15664  metcnp  15665  metcnp2  15666  metcn  15667  txmetcnp  15671  txmetcn  15672  metcnpd  15673  bl2ioo  15703  addcncntoplem  15714  elcncf  15726  elcncf2  15727  ivthdec  15797  ellimc3apf  15813  cnlimcim  15824  dveflem  15879  ply1termlem  15895  sincosq2sgn  15981  sinq12gt0  15984  logltb  16029  ltexp2  16099  birthdaylem3  16149  wilthlem1  16154  ppiublem1  16213  prmefexple  16230  bposlem1  16233  lgsdilem  16268  lgsdir2lem4  16272  lgsdir2  16274  lgsne0  16279  lgsabs1  16280  gausslemma2dlem3  16304  gausslemma2dlem7  16309  lgseisenlem3  16313  lgsquad3  16325  2lgslem1a  16329  2lgslem3c  16336  2lgslem3d  16337  2lgsoddprmlem4  16353  2sqlem7  16362  2sqlem8a  16363  uhgreq12g  16439  isuhgropm  16444  uhgr0e  16445  upgrop  16467  uhgrvtxedgiedgb  16506  isuspgropen  16527  isusgropen  16528  uhgr2edg  16569  issubgr2  16621  uhgrspansubgrlem  16639  vtxd0nedgbfi  16662  1loopgrvd0fi  16669  iswlk  16686  upgriswlkdc  16723  istrl  16748  iseupth  16810  eupth2lem2dc  16822  eupth2lem3lem3fi  16833  eupth2lem3lem4fi  16836  eupth2lem3lem7fi  16837  cbvrald  16938  bj-nalset  17043  bj-sels  17062  bj-nnelirr  17101  stnot  17161  isomninnlem  17201  iswomninnlem  17221  iswomni0  17223  ismkvnnlem  17224