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  801  con1biidc  885  pm4.54dc  910  dn1dc  969  dedlem0a  977  dfifp3dc  991  dfifp4dc  992  dfifp5dc  993  3bior2fd  1391  xorbi12d  1427  nbbndc  1439  eleq12d  2305  neeq12d  2434  neleq12d  2515  raleqbi1dv  2755  rexeqbi1dv  2756  reueqd  2757  rmoeqd  2758  raleqbidv  2759  rexeqbidv  2760  raleqbidva  2761  rexeqbidva  2762  eueq3dc  2994  sbc19.21g  3114  sbcabel  3128  sbcel1g  3160  sbceq1g  3161  sbcel2g  3162  sbceq2g  3163  sbccsb2g  3171  sbcco3g  3199  sseq12d  3273  raaanlem  3618  sbcssg  3622  ralsng  3734  2ralunsn  3908  csbunig  3927  disjeq12d  4099  breq123d  4128  sbcbr12g  4170  sbcbr1g  4171  sbcbr2g  4172  treq  4219  nalset  4245  exmidsssn  4320  copsex4g  4368  onsucb  4630  posng  4827  csbxpg  4836  sbcrel  4841  csbcnvg  4944  eliniseg  5137  brcodir  5155  csbrng  5229  sbcfung  5381  fneq12d  5453  feq12d  5503  feq123d  5504  sbcfng  5511  sbcfg  5512  f1osng  5662  csbfv12g  5715  funimass4  5732  dmfco  5750  eqfnfv  5780  eqfnfv2  5781  fneqeql2  5792  fvimacnvi  5797  funimass3  5799  fniniseg  5803  unpreima  5807  ralrnmpt  5824  rexrnmpt  5825  dffo3  5829  fmptco  5848  fressnfv  5876  eufnfv  5922  foima2  5930  fnunirn  5946  dff13  5947  f1elima  5952  cocan1  5966  cocan2  5967  fliftel  5972  fliftf  5978  isoresbr  5988  isoini  5997  f1oiso  6005  f1ofveu  6046  mpoeq123dva  6122  ovid  6178  ov  6181  ovg  6201  ovelrn  6211  caovord2d  6232  ofrfval2  6292  offveqb  6295  eqop  6384  reldm  6393  f1od2  6444  suppval1  6452  suppssrst  6474  suppssrgst  6475  mpoxopoveq  6484  mpoxopovel  6485  tpostpos  6508  smoiso  6546  frecabcl  6643  frecsuclem  6650  nnaordr  6756  nnaword  6757  nnaordex  6774  ereq1  6787  brdifun  6807  erth2  6827  qliftfun  6864  brecop  6872  elmapg  6908  elpmg  6911  mapsnd  6936  dom2lem  7024  xpcomco  7090  pw2f1odclem  7100  php5fin  7152  funisfsupp  7257  ffsuppbi  7266  elfi2  7272  supisolem  7312  inflbti  7328  inl11  7369  ismkvnex  7459  mkvprop  7462  nninfwlporlemd  7476  exmidfodomrlemreseldju  7516  ltapig  7669  ltmpig  7670  nlt1pig  7672  mulcmpblnq  7699  ltsonq  7729  lt2addnq  7735  lt2mulnq  7736  archnqq  7748  prarloclemarch  7749  ltrnqg  7751  mulcmpblnq0  7775  preqlu  7803  genpdflem  7838  addnqprllem  7858  addnqprulem  7859  addlocprlemgt  7865  appdivnq  7894  mulnqprl  7899  mulnqpru  7900  mullocprlem  7901  distrlem4prl  7915  distrlem4pru  7916  1idprl  7921  1idpru  7922  ltexprlemloc  7938  cauappcvgprlemladdrl  7988  cauappcvgprlemladd  7989  cauappcvgprlem1  7990  archrecnq  7994  caucvgprlemnkj  7997  caucvgprprlemexb  8038  addcmpblnr  8070  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1  8112  srpospr  8114  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  map2psrprg  8136  ltresr  8170  axcaucvglemres  8230  eqlelt  8376  cnegexlem1  8465  negeu  8481  subadd2  8494  subcan2  8515  addrsub  8661  ltaddneg  8716  ltaddnegr  8717  ltadd1  8721  leadd2  8723  ltsubadd  8724  lesubadd  8726  ltaddsub2  8729  leaddsub2  8731  ltaddpos  8744  lesub2  8749  ltsub2  8751  ltnegcon1  8755  ltnegcon2  8756  lenegcon1  8758  lenegcon2  8759  addge01  8764  addge02  8765  suble0  8768  leaddle0  8769  lesub0  8771  eqord2  8776  sublt0d  8862  recexre  8870  reaplt  8880  reapltxor  8881  reapneg  8889  remulext1  8891  apreim  8895  apcotr  8899  apadd2  8901  addext  8902  apsub1  8934  mulcanap2d  8954  diveqap0  8976  diveqap1  8999  apmul2  9083  ltmul2  9150  lemul2  9151  ltmulgt11  9158  ltmulgt12  9159  gt0div  9164  ge0div  9165  ltmuldiv  9168  ltrec1  9182  lerec2  9183  ledivdiv  9184  ltdiv23  9186  lediv23  9187  suprleubex  9248  creur  9253  creui  9254  nn1suc  9276  nnrecl  9514  fcdmnn0fsuppg  9571  znnsub  9649  zgt0ge1  9656  zltlen  9677  nn0n0n1ge2b  9678  nn0le2is012  9681  btwnnz  9693  gtndiv  9694  prime  9698  eluz2  9880  indstr2  9962  negm  9968  nn01to3  9970  qapne  9992  qltlen  9993  qreccl  9995  irrmulap  10001  divlt1lt  10078  divle1le  10079  nnledivrp  10120  xnn0xadd0  10222  xltadd2  10232  xsubge0  10236  xlesubadd  10238  iccid  10280  elioc2  10291  elico2  10292  elicc2  10293  elfz2  10371  fzen  10400  fzsubel  10418  elfzp1  10431  fzpr  10436  fzrevral2  10465  fzrevral3  10466  nn0disj  10497  2ffzeq  10500  fzosplitsni  10606  fvinim0ffz  10612  ioo0  10646  ico0  10648  ioc0  10649  modq0  10718  negqmod0  10720  zmodidfzo  10742  frecuzrdgtcl  10801  nn0ennn  10822  nninfinf  10832  sq11  11001  nn0le2msqd  11109  nn0opth2d  11113  hashen  11175  zfz1isolem1  11240  zfz1iso  11241  csbwrdg  11282  wrdnval  11283  eqwrd  11293  ccat0  11312  ccatws1lenp1bg  11351  swrd0g  11380  swrdspsleq  11387  pfxeq  11416  pfxsuffeqwrdeq  11418  pfxsuff1eqwrdeq  11419  ccatopth2  11437  wrd2ind  11443  2shfti  11544  cjap  11619  cnreim  11691  rexfiuz  11702  rexanuz2  11704  abs00ap  11775  absext  11776  sqabs  11795  abslt  11801  absle  11802  absdiflt  11805  absdifle  11806  lenegsq  11808  minmax  11943  ltmininf  11948  mingeb  11955  xrminmax  11978  xrmin1inf  11980  xrmin2inf  11981  xrltmininf  11983  xrlemininf  11984  clim  11994  clim0c  11999  climrecvg1n  12061  zsumdc  12098  fsum2dlemstep  12148  binomlem  12197  pwm1geoserap1  12222  zproddc  12293  efieq  12449  sin01bnd  12471  cos01bnd  12472  dvdsval2  12504  modm1div  12514  zdvdsdc  12526  modmulconst  12537  dvdsaddr  12551  dvdsabseq  12561  fzocongeq  12572  zeo3  12582  odd2np1  12587  oddp1d2  12604  zob  12605  oddm1d2  12606  nnoddm1d2  12624  divalgb  12639  divalgmod  12641  modremain  12643  bits0  12662  bitsp1e  12666  bitsp1o  12667  bitscmp  12672  bitsinv1lem  12675  gcdn0gt0  12702  bezoutlemstep  12721  dvdssq  12755  nn0seqcvgd  12766  algcvgblem  12774  lcmdvds  12804  lcmgcdeq  12808  coprmdvds  12817  qredeq  12821  congr  12825  isprm2  12842  isprm3  12843  prmdvdsexp  12873  prmdvdsexpb  12874  prmexpb  12876  prmfac1  12877  cncongrprm  12882  oddpwdclemxy  12894  oddpwdclemodd  12897  qnumdenbi  12917  qnumgt0  12923  hashdvds  12946  crth  12949  fermltl  12959  modprminveq  12976  pcpremul  13019  pc2dvds  13056  pcz  13058  prmpwdvds  13081  4sqlem16  13132  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemodife  13187  ballotfilemrv1  13211  ballotfilemrv2  13212  ballotfilem1ri  13225  oddennn  13230  ctinfomlemom  13265  mgm1  13636  ismhm  13719  mhmpropd  13724  issubm  13730  issubm2  13731  grpsubrcan  13839  grplactcnv  13860  grp1  13864  eqgval  13979  eqgid  13982  quselbasg  13986  isghm  13999  conjnmzb  14036  iscmn  14049  eqgabl  14086  prdsbasmpt  14125  prdsbasmpt2  14133  rngmneg1  14189  rngmneg2  14190  rngpropd  14197  rngen1zr  14203  srgen1zr0  14234  ringideu  14263  ringpropd  14284  crngpropd  14285  dvdsrd  14342  dvdsr02  14353  opprunitd  14358  crngunit  14359  unitpropdg  14396  rhmunitinv  14426  isnzr2  14432  issubrng  14448  resrhm2b  14498  aprval  14532  aprunit  14533  isdrngtap  14547  opprdrng  14561  islmod  14568  islssm  14634  islssmg  14635  ellspsn  14694  isridl  14781  zrhrhmb  14899  zndvds  14926  znleval  14930  istopg  14993  eltg  15046  eltg2  15047  tgss2  15073  bastop1  15077  bastop2  15078  iscld  15097  isnei  15138  neiint  15139  iscn  15191  iscnp  15193  iscnp3  15197  tgcn  15202  ssidcn  15204  lmbr2  15208  lmbrf  15209  cnnei  15226  cnrest2  15230  eltx  15253  imasnopn  15293  ispsmet  15317  ismet  15338  isxmet  15339  metn0  15372  xmetres2  15373  elbl3ps  15388  elbl3  15389  xblpnfps  15392  xblpnf  15393  elmopn2  15443  metss  15488  bdxmet  15495  metrest  15500  xmetxp  15501  xmetxpbl  15502  metcnp3  15505  metcnp  15506  metcnp2  15507  metcn  15508  txmetcnp  15512  txmetcn  15513  metcnpd  15514  bl2ioo  15544  addcncntoplem  15555  elcncf  15567  elcncf2  15568  ivthdec  15638  ellimc3apf  15654  cnlimcim  15665  dveflem  15720  ply1termlem  15736  sincosq2sgn  15821  sinq12gt0  15824  logltb  15868  ltexp2  15935  wilthlem1  15977  lgsdilem  16029  lgsdir2lem4  16033  lgsdir2  16035  lgsne0  16040  lgsabs1  16041  gausslemma2dlem3  16065  gausslemma2dlem7  16070  lgseisenlem3  16074  lgsquad3  16086  2lgslem1a  16090  2lgslem3c  16097  2lgslem3d  16098  2lgsoddprmlem4  16114  2sqlem7  16123  2sqlem8a  16124  uhgreq12g  16200  isuhgropm  16205  uhgr0e  16206  upgrop  16228  uhgrvtxedgiedgb  16267  isuspgropen  16288  isusgropen  16289  uhgr2edg  16330  issubgr2  16382  uhgrspansubgrlem  16400  vtxd0nedgbfi  16423  1loopgrvd0fi  16430  iswlk  16447  upgriswlkdc  16484  istrl  16509  iseupth  16571  eupth2lem2dc  16583  eupth2lem3lem3fi  16594  eupth2lem3lem4fi  16597  eupth2lem3lem7fi  16598  cbvrald  16699  bj-nalset  16804  bj-sels  16823  bj-nnelirr  16862  isomninnlem  16953  iswomninnlem  16973  iswomni0  16975  ismkvnnlem  16976