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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  462  anbi12d  473  orbi12d  793  con1biidc  877  pm4.54dc  902  dn1dc  960  dedlem0a  968  xorbi12d  1382  nbbndc  1394  eleq12d  2248  neeq12d  2367  neleq12d  2448  raleqbi1dv  2680  rexeqbi1dv  2681  reueqd  2682  rmoeqd  2683  raleqbidv  2684  rexeqbidv  2685  raleqbidva  2686  rexeqbidva  2687  eueq3dc  2911  sbc19.21g  3031  sbcabel  3044  sbcel1g  3076  sbceq1g  3077  sbcel2g  3078  sbceq2g  3079  sbccsb2g  3087  sbcco3g  3114  sseq12d  3186  raaanlem  3528  sbcssg  3532  ralsng  3632  2ralunsn  3798  csbunig  3817  disjeq12d  3989  breq123d  4017  sbcbr12g  4058  sbcbr1g  4059  sbcbr2g  4060  treq  4107  nalset  4133  exmidsssn  4202  copsex4g  4247  onsucb  4502  posng  4698  csbxpg  4707  sbcrel  4712  csbcnvg  4811  eliniseg  4998  brcodir  5016  csbrng  5090  sbcfung  5240  fneq12d  5308  feq12d  5355  feq123d  5356  sbcfng  5363  sbcfg  5364  f1osng  5502  csbfv12g  5551  funimass4  5566  dmfco  5584  eqfnfv  5613  eqfnfv2  5614  fneqeql2  5625  fvimacnvi  5630  funimass3  5632  fniniseg  5636  rexsupp  5640  unpreima  5641  ralrnmpt  5658  rexrnmpt  5659  dffo3  5663  fmptco  5682  fressnfv  5703  eufnfv  5747  foima2  5752  fnunirn  5767  dff13  5768  f1elima  5773  cocan1  5787  cocan2  5788  fliftel  5793  fliftf  5799  isoresbr  5809  isoini  5818  f1oiso  5826  f1ofveu  5862  mpoeq123dva  5935  ovid  5990  ov  5993  ovg  6012  ovelrn  6022  caovord2d  6043  ofrfval2  6098  offveqb  6101  eqop  6177  reldm  6186  f1od2  6235  mpoxopoveq  6240  mpoxopovel  6241  tpostpos  6264  smoiso  6302  frecabcl  6399  frecsuclem  6406  nnaordr  6510  nnaword  6511  nnaordex  6528  ereq1  6541  brdifun  6561  erth2  6579  qliftfun  6616  brecop  6624  elmapg  6660  elpmg  6663  dom2lem  6771  xpcomco  6825  php5fin  6881  elfi2  6970  supisolem  7006  inflbti  7022  inl11  7063  ismkvnex  7152  mkvprop  7155  nninfwlporlemd  7169  exmidfodomrlemreseldju  7198  ltapig  7336  ltmpig  7337  nlt1pig  7339  mulcmpblnq  7366  ltsonq  7396  lt2addnq  7402  lt2mulnq  7403  archnqq  7415  prarloclemarch  7416  ltrnqg  7418  mulcmpblnq0  7442  preqlu  7470  genpdflem  7505  addnqprllem  7525  addnqprulem  7526  addlocprlemgt  7532  appdivnq  7561  mulnqprl  7566  mulnqpru  7567  mullocprlem  7568  distrlem4prl  7582  distrlem4pru  7583  1idprl  7588  1idpru  7589  ltexprlemloc  7605  cauappcvgprlemladdrl  7655  cauappcvgprlemladd  7656  cauappcvgprlem1  7657  archrecnq  7661  caucvgprlemnkj  7664  caucvgprprlemexb  7705  addcmpblnr  7737  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1  7779  srpospr  7781  caucvgsrlemcau  7791  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  map2psrprg  7803  ltresr  7837  axcaucvglemres  7897  eqlelt  8042  cnegexlem1  8130  negeu  8146  subadd2  8159  subcan2  8180  addrsub  8326  ltaddneg  8379  ltaddnegr  8380  ltadd1  8384  leadd2  8386  ltsubadd  8387  lesubadd  8389  ltaddsub2  8392  leaddsub2  8394  ltaddpos  8407  lesub2  8412  ltsub2  8414  ltnegcon1  8418  ltnegcon2  8419  lenegcon1  8421  lenegcon2  8422  addge01  8427  addge02  8428  suble0  8431  leaddle0  8432  lesub0  8434  eqord2  8439  sublt0d  8525  recexre  8533  reaplt  8543  reapltxor  8544  reapneg  8552  remulext1  8554  apreim  8558  apcotr  8562  apadd2  8564  addext  8565  apsub1  8597  mulcanap2d  8617  diveqap0  8637  diveqap1  8660  apmul2  8744  ltmul2  8811  lemul2  8812  ltmulgt11  8819  ltmulgt12  8820  gt0div  8825  ge0div  8826  ltmuldiv  8829  ltrec1  8843  lerec2  8844  ledivdiv  8845  ltdiv23  8847  lediv23  8848  suprleubex  8909  creur  8914  creui  8915  nn1suc  8936  nnrecl  9172  znnsub  9302  zgt0ge1  9309  zltlen  9329  nn0n0n1ge2b  9330  nn0le2is012  9333  btwnnz  9345  gtndiv  9346  prime  9350  eluz2  9532  indstr2  9607  negm  9613  nn01to3  9615  qapne  9637  qltlen  9638  qreccl  9640  divlt1lt  9722  divle1le  9723  nnledivrp  9764  xnn0xadd0  9865  xltadd2  9875  xsubge0  9879  xlesubadd  9881  iccid  9923  elioc2  9934  elico2  9935  elicc2  9936  elfz2  10013  fzen  10040  fzsubel  10057  elfzp1  10069  fzpr  10074  fzrevral2  10103  fzrevral3  10104  nn0disj  10135  2ffzeq  10138  fzosplitsni  10232  fvinim0ffz  10238  ioo0  10257  ico0  10259  ioc0  10260  modq0  10326  negqmod0  10328  zmodidfzo  10350  frecuzrdgtcl  10409  nn0ennn  10430  sq11  10589  nn0le2msqd  10694  nn0opth2d  10698  hashen  10759  zfz1isolem1  10815  zfz1iso  10816  2shfti  10835  cjap  10910  cnreim  10982  rexfiuz  10993  rexanuz2  10995  abs00ap  11066  absext  11067  sqabs  11086  abslt  11092  absle  11093  absdiflt  11096  absdifle  11097  lenegsq  11099  minmax  11233  ltmininf  11238  mingeb  11245  xrminmax  11268  xrmin1inf  11270  xrmin2inf  11271  xrltmininf  11273  xrlemininf  11274  clim  11284  clim0c  11289  climrecvg1n  11351  zsumdc  11387  fsum2dlemstep  11437  binomlem  11486  pwm1geoserap1  11511  zproddc  11582  efieq  11738  sin01bnd  11760  cos01bnd  11761  dvdsval2  11792  modm1div  11802  zdvdsdc  11814  modmulconst  11825  dvdsaddr  11839  dvdsabseq  11847  fzocongeq  11858  zeo3  11867  odd2np1  11872  oddp1d2  11889  zob  11890  oddm1d2  11891  nnoddm1d2  11909  divalgb  11924  divalgmod  11926  modremain  11928  gcdn0gt0  11973  bezoutlemstep  11992  dvdssq  12026  nn0seqcvgd  12035  algcvgblem  12043  lcmdvds  12073  lcmgcdeq  12077  coprmdvds  12086  qredeq  12090  congr  12094  isprm2  12111  isprm3  12112  prmdvdsexp  12142  prmdvdsexpb  12143  prmexpb  12145  prmfac1  12146  cncongrprm  12151  oddpwdclemxy  12163  oddpwdclemodd  12166  qnumdenbi  12186  qnumgt0  12192  hashdvds  12215  crth  12218  fermltl  12228  modprminveq  12244  pcpremul  12287  pc2dvds  12323  pcz  12325  prmpwdvds  12347  oddennn  12387  ctinfomlemom  12422  mgm1  12743  ismhm  12807  mhmpropd  12811  issubm  12817  issubm2  12818  grpsubrcan  12905  grplactcnv  12926  grp1  12930  eqgval  13035  eqgid  13038  iscmn  13049  srgen1zr  13124  ringideu  13153  ringpropd  13170  crngpropd  13171  dvdsrd  13216  dvdsr02  13227  opprunitd  13232  crngunit  13233  unitpropdg  13270  aprval  13293  istopg  13390  eltg  13445  eltg2  13446  tgss2  13472  bastop1  13476  bastop2  13477  iscld  13496  isnei  13537  neiint  13538  iscn  13590  iscnp  13592  iscnp3  13596  tgcn  13601  ssidcn  13603  lmbr2  13607  lmbrf  13608  cnnei  13625  cnrest2  13629  eltx  13652  imasnopn  13692  ispsmet  13716  ismet  13737  isxmet  13738  metn0  13771  xmetres2  13772  elbl3ps  13787  elbl3  13788  xblpnfps  13791  xblpnf  13792  elmopn2  13842  metss  13887  bdxmet  13894  metrest  13899  xmetxp  13900  xmetxpbl  13901  metcnp3  13904  metcnp  13905  metcnp2  13906  metcn  13907  txmetcnp  13911  txmetcn  13912  metcnpd  13913  bl2ioo  13935  addcncntoplem  13944  elcncf  13953  elcncf2  13954  ivthdec  14015  ellimc3apf  14022  cnlimcim  14033  dveflem  14080  sincosq2sgn  14141  sinq12gt0  14144  logltb  14188  ltexp2  14253  lgsdilem  14321  lgsdir2lem4  14325  lgsdir2  14327  lgsne0  14332  lgsabs1  14333  2sqlem7  14350  2sqlem8a  14351  cbvrald  14422  bj-nalset  14529  bj-sels  14548  bj-nnelirr  14587  isomninnlem  14660  iswomninnlem  14679  iswomni0  14681  ismkvnnlem  14682