Theorem biimtrdi 256

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

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

Assertion

Ref	Expression
biimtrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem biimtrdi

Step	Hyp	Ref	Expression
1		biimtrdi.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 232	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ax12i  2000  sb4a  2512  hbsb2  2514  dfsb2  2525  2eu2  2680  reu6  3687  nrmod  3843  2reu2  3850  disjel  4413  disjpss  4417  preq12b  4808  prneimg  4812  preqsnd  4817  elinti  4919  zfrepclf  5247  exnelv  5270  dtruALT2  5336  opth1g  5451  sbcop1  5462  snopeqop  5482  propeqop  5483  otsndisj  5496  otiunsndisj  5497  iunopeqop  5498  iunopeqopOLD  5499  po2ne  5579  soasym  5596  elrelb  5780  elreldm  5922  dfres3  5980  relcnvtrgOLD  6276  relresfldOLD  6286  elpredimg  6326  ordtr2  6415  ordssun  6474  funopg  6583  funimass2  6634  f0dom0  6777  elfv2ex  6939  fveqdmss  7089  eldmrexrnb  7103  fvcofneq  7104  funopsn  7162  funopsnOLD  7163  funopdmsn  7165  funsndifnop  7166  elunirn  7265  oprabidw  7461  oprabid  7462  brfvopab  7487  limuni3  7873  peano5  7915  resf1ext2b  7957  op1steq  8055  el2mpocsbcl  8107  bropopvvv  8112  bropfvvvv  8114  f1o2ndf1  8146  frxp  8151  fnwelem  8156  poxp2  8173  suppimacnv  8205  fvn0elsuppb  8212  suppfnss  8220  reldmtpos  8265  rntpos  8270  seqomlem2  8475  oaordi  8568  oa00  8581  oalimcl  8582  omeulem1  8604  nnaordi  8641  ecopovtrn  8855  undifixp  8976  mapdom2  9181  unxpdomlem3  9263  en1eqsn  9280  infssuni  9349  wdompwdom  9585  preleqg  9629  opthreg  9632  inf3lemd  9641  inf3lem2  9643  inf3lem6  9647  cnfcomlem  9713  cnfcom3  9718  karden  9972  kardenOLD  9973  carden2a  10060  alephdom  10173  dfac5lem4  10218  dfac12r  10238  kmlem2  10243  kmlem12  10253  cfslb2n  10359  alephsing  10367  fin23lem30  10433  fin1a2lem6  10496  fin1a2lem13  10503  axcc2lem  10527  domtriomlem  10533  axdc3lem2  10542  axdc4lem  10546  brdom6disj  10624  alephexp1  10677  pwfseq  10762  addnidpi  10999  indpi  11005  nqereu  11027  ltsonq  11067  distrlem5pr  11125  addcanpr  11144  suplem1pr  11150  suplem2pr  11151  ltsrpr  11175  ltsosr  11192  sqgt0sr  11204  leltne  11412  ltnsym  11421  ltlen  11424  eqlei  11433  eqlei2  11434  infm3  12289  nnunb  12615  0mnnnnn0  12651  elnnnn0b  12663  nn0ge2m1nn  12689  nn0le2is012  12776  btwnz  12815  uz11  13003  xrleltne  13287  xltnegi  13359  xnn0lenn0nn0  13388  xnn0xadd0  13390  xmulasslem2  13425  reltxrnmnf  13486  icogelb  13540  iccleub  13545  uznfz  13757  2ffzeq  13796  elfzonlteqm1  13889  elfzo0l  13904  fzoopth  13910  elfznelfzob  13922  elfzr  13929  elfzlmr  13930  injresinjlem  13938  injresinj  13939  fleqceilz  14007  modadd1  14061  modmul1  14080  modirr  14098  addmodlteq  14102  uzrdgfni  14114  fsuppmapnn0fiub0  14149  fsuppmapnn0ub  14151  seqf1o  14199  expnngt1  14398  hashrabsn01  14530  hashrabsn1  14531  hash1snb  14577  hash1n0  14579  hashf1lem2  14614  hash2prde  14628  hash2prd  14633  hash2pwpr  14634  hashle2pr  14635  hashle2prv  14636  hashge2el2dif  14638  hashge2el2difr  14639  hash3tpde  14651  fundmge2nop0  14660  ffz0iswrd  14699  ccatrcl1  14754  pfxsuff1eqwrdeq  14862  wrdind  14885  wrd2ind  14886  swrdccatin1  14888  swrdccat3blem  14902  2cshwcshw  14990  cshwcsh2id  14993  cshimadifsn  14994  2swrd2eqwrdeq  15121  wwlktovf  15124  wwlktovfo  15126  s3sndisj  15135  s3iunsndisj  15136  relexpindlem  15231  rexico  15536  lo1le  15834  fsum2dlem  15951  ntrivcvg  16081  fprodss  16130  fprod2dlem  16162  0dvds  16461  mod2eq1n2dvds  16532  opoe  16548  omoe  16549  opeo  16550  omeo  16551  m1exp1  16561  nn0enne  16562  nn0o1gt2  16566  gcdneg  16709  dfgcd2  16734  algcvga  16769  eucalglt  16775  lcmf  16823  coprmdvds  16843  divgcdcoprmex  16856  cncongr1  16857  prm2orodd  16881  prm23lt5  17007  pockthi  17100  prmreclem5  17113  ramtcl2  17204  cshwrepswhash1  17295  f1ocpbl  17712  f1ovscpbl  17713  f1olecpbl  17714  monhom  17925  epihom  17932  inveq  17964  invcoisoid  17982  isocoinvid  17983  ciclcl  17992  cicrcl  17993  isinitoi  18189  istermoi  18190  2initoinv  18200  2termoinv  18207  setciso  18281  embedsetcestrclem  18346  ipopos  18725  mgmpropd  18844  gsumval2a  18889  ismnddef  18940  dfgrp2e  19189  symg2bas  19622  snsymgefmndeq  19624  symgvalstruct  19626  symgfix2  19645  gsmsymgreq  19661  pmtrdifellem4  19708  mndodcongi  19772  pj1eu  19925  cycsubmcmn  20118  dprd2da  20273  rngimf1o  20699  rngimrnghm  20700  c0snmgmhm  20707  0ring01eq  20795  elrngchom  20891  rnghmsubcsetclem1  20898  rnghmsubcsetclem2  20899  rngcid  20902  rngcinv  20904  rngciso  20905  funcrngcsetcALT  20908  zrinitorngc  20909  zrtermorngc  20910  elringchom  20920  rhmsubcsetclem1  20927  rhmsubcsetclem2  20928  ringcid  20931  rhmsubcrngclem1  20933  rhmsubcrngclem2  20934  ringciso  20939  zrtermoringc  20942  rhmsubclem3  20954  rhmsubclem4  20955  lmodfopnelem1  21188  lspdisjb  21419  lspsnsubn0  21433  rngqiprngfulem2  21623  irinitoringc  21800  obs2ss  22050  mamufacex  22726  mat0dim0  22797  mat0dimid  22798  mat0dimscm  22799  dmatmat  22824  scmatmat  22839  mat1scmat  22869  1mavmul  22878  mavmulsolcl  22881  gsummatr01  22989  matunitlindf  23011  cpmatpmat  23043  cpmadugsumlemF  23209  tg2  23298  tgcl  23302  neii1  23439  neii2  23441  neindisj2  23456  perfopn  23518  ordtbas2  23524  pnfnei  23553  mnfnei  23554  llyidm  23822  txlm  23982  qtopuni  24036  tgqtop  24046  isfild  24192  snfil  24198  fbunfip  24203  fgss2  24208  fmco  24295  fbflim2  24311  cnpflf2  24334  fcfelbas  24370  fcfneii  24371  alexsubALTlem2  24382  alexsubALT  24385  tgpconncompeqg  24446  tsmscl  24469  tngngpim  24993  tgioo  25130  xrsmopn  25147  iccntr  25156  reconnlem2  25162  addcnlem  25199  htpycn  25309  phtpyhtpy  25318  pi1blem  25375  fgcfil  25607  ioombl1lem4  25897  dyadmbl  25936  itg2gt0  26096  ditgneg  26192  dvivthlem1  26343  coeeq2  26576  aannenlem2  26671  sineq0  26867  efif1o  26889  xrlimcnp  27311  vmacl  27460  efvmacl  27462  vmalelog  27547  dchrelbasd  27581  lgsqr  27693  lgsqrmodndvds  27695  gausslemma2dlem0i  27706  2lgslem2  27737  2lgs  27749  2lgsoddprmlem3  27756  2sqnn  27781  2sqreultlem  27789  2sqreultblem  27790  2sqreunnltlem  27792  2sqreunnltblem  27793  ltsintdifex  28033  ltsres  28034  nosepnelem  28051  nolt02o  28067  ltlesnd  28147  negsprop  28436  mulsprop  28531  onnolt  28667  onlts  28668  n0subs  28764  bdaypw2n0bndlem  28864  bdaypw2n0bnd  28865  bdayfinbndlem2  28869  elntg2  29578  uhgr0vb  29665  umgrupgr  29696  umgrnloopv  29699  umgredgprv  29700  umgrislfupgrlem  29715  umgredg  29731  uspgrushgr  29773  uspgrupgr  29774  usgruspgr  29776  usgredgprvALT  29791  usgrnloopvALT  29797  uhgr2edg  29804  edg0usgr  29849  egrsubgr  29873  0uhgrsubgr  29875  uhgrspansubgrlem  29886  nbuhgr  29939  cusgrsize2inds  30049  cusgrfilem2  30052  vtxdg0v  30069  1loopgrnb0  30098  vtxdginducedm1lem4  30138  wlkvtxeledg  30219  wlkeq  30229  wlkl1loop  30233  wlk1walk  30234  upgrwlkedg  30237  uspgr2wlkeq  30241  wlkv0  30245  wlkonl1iedg  30259  wlkon2n0  30260  wlkp1lem8  30274  wlkp1  30275  lfgrwlkprop  30285  lfgrwlknloop  30287  2pthnloop  30332  upgrwlkdvde  30338  spthonepeq  30353  uhgrwkspthlem2  30355  usgr2wlkneq  30357  usgr2trlncl  30361  usgr2trlspth  30362  pthdlem2lem  30368  clwlkcompbp  30384  uspgrn2crct  30412  wwlks  30439  wwlknbp  30446  0enwwlksnge1  30468  wwlkswwlksn  30469  wlklnwwlkln1  30472  wwlksnextproplem3  30515  wwlksnextprop  30516  wspthsnonn0vne  30521  wspn0  30528  2pthon3v  30547  umgr2adedgspth  30552  rusgr0edg  30580  clwwlkccat  30596  clwlkclwwlklem2fv2  30602  clwlkclwwlklem2a4  30603  clwlkclwwlklem2  30606  clwlkclwwlkflem  30610  clwwlknp  30643  clwwlkwwlksb  30660  clwwlkext2edg  30662  erclwwlkneqlen  30674  hashecclwwlkn1  30683  umgrhashecclwwlk  30684  clwwlknonwwlknonb  30712  upgr1wlkdlem1  30751  upgr3v3e3cycl  30796  uhgr3cyclexlem  30797  1conngr  30810  conngrv2edg  30811  eupth2lem3lem4  30847  eulercrct  30858  isfrgr  30876  frgr3vlem2  30890  1to2vfriswmgr  30895  1to3vfriswmgr  30896  frgrncvvdeqlem9  30923  frgrwopreg  30939  frgr2wwlkeqm  30947  2wspmdisj  30953  numclwwlk1lem2f  30971  frgrreggt1  31009  frgrregord013  31011  frgrregord13  31012  l2p  31096  nmlno0lem  31410  normgt0  31744  ocin  31913  nmlnop0iALT  32612  nmopun  32631  cvpss  32902  cvnbtwn  32903  atcvati  33003  mdsymlem6  33025  iunrnmptss  33216  expgt0b  33464  wrdt2ind  33572  irngssv  34376  issgon  34811  mbfmcnt  34956  ballotlemfc0  35181  ballotlemfcc  35182  reu6f  35765  jaeqifi  35768  kardcard2b  35907  dfk12  35969  dfk22  35970  dfk32  35971  satfv0  36247  satfv0fun  36260  fmla1  36276  gonarlem  36283  gonar  36284  goalrlem  36285  goalr  36286  fmla0disjsuc  36287  satffunlem  36290  satffunlem1lem1  36291  satffunlem2lem1  36293  satfun  36300  satfv0fvfmla0  36302  sategoelfv  36309  mthmblem  36469  pprodss4v  36776  funpartfun  36837  funpartfv  36839  5segofs  36901  btwnxfr  36951  brofs2  36972  brifs2  36973  btwnconn1  36996  segleantisym  37010  broutsideof2  37017  outsidene1  37018  outsidene2  37019  funray  37035  lineunray  37042  cldbnd  37244  bj-imdirval3  38248  topdifinffinlem  38413  isbasisrelowllem1  38421  isbasisrelowllem2  38422  relowlpssretop  38430  inunissunidif  38441  pibt2  38483  poimir  38714  volsupnfl  38726  itg2addnclem  38732  findcard4  38775  cover2  38792  sdclem2  38819  fdc  38822  sstotbnd3  38853  heibor1  38887  clmgmOLD  38928  smgrpmgm  38941  smgrpassOLD  38942  dvrunz  39031  0rngo  39104  mopickr  39446  sucmapleftuniq  39565  lsatcvat  40250  lshpkrex  40318  cmtbr3N  40454  atn0  40508  atnle  40517  cvlsupr4  40545  cvlsupr5  40546  cvlsupr6  40547  cvrval4N  40614  cvratlem  40621  2llnjN  40767  2lplnj  40820  linepsubN  40952  elpaddatiN  41005  elpcliN  41093  pclcmpatN  41101  ldilval  41313  ltrnu  41321  cdleme18d  41495  tendotp  41961  tendof  41963  tendovalco  41965  diatrl  42244  diaintclN  42258  dvheveccl  42312  dibintclN  42367  dihord6apre  42456  dihmeetlem1N  42490  dihpN  42536  dihintcl  42544  dochkrshp4  42589  oexpreposd  43522  pw2f1ocnv  44187  iocinico  44357  onsucf1olem  44415  succlg  44473  oacl2g  44475  omabs2  44477  omcl2  44478  naddcnfcom  44511  naddcnfass  44514  safesnsupfidom1o  44561  infordmin  44676  pr2cv  44692  expgrowthi  45460  iotavalsb  45559  bi23imp1  45620  ioogtlb  46649  iocgtlb  46656  iocleub  46657  icoltub  46662  iooltub  46664  stoweidlem31  47183  oppr  48242  funressnfv  48255  fsetsniunop  48261  fsetsnf1  48264  aiotaexim  48310  eu2ndop1stv  48337  afvelrnb0  48376  otiunsndisjX  48491  el1fzopredsuc  48538  2ffzoeq  48540  uniimaprimaeqfv  48606  elsetpreimafveqfv  48616  iccpartimp  48641  iccpartrn  48654  iccpartf  48655  iccpartnel  48662  fargshiftf  48664  fargshiftfo  48666  ichnfimlem  48687  ichnfim  48688  ichreuopeq  48697  sprel  48708  sprsymrelfvlem  48714  sprsymrelfolem2  48717  prproropf1olem4  48730  prprelb  48740  poprelb  48748  fmtnofac1  48797  prmdvdsfmtnof1lem2  48812  31prm  48824  lighneallem3  48834  ppivalnnnprm  48855  nn0o1gt2ALTV  48934  nn0oALTV  48936  odd2prm2  48958  mogoldbblem  48960  fpprbasnn  48969  fpprnn  48970  sbgoldbaltlem1  49019  nnsum3primesle9  49034  bgoldbtbndlem1  49045  bgoldbtbndlem2  49046  elclnbgrelnbgr  49065  grimedgi  49176  grtriproplem  49179  grtriprop  49181  cycl3grtrilem  49186  cycl3grtri  49187  isubgr3stgrlem8  49213  gpgvtxel2  49288  gpgedgiov  49305  gpgedg2iv  49307  gpgprismgr4cycllem7  49341  pgnbgreunbgrlem1  49353  pgnbgreunbgrlem2lem1  49354  pgnbgreunbgrlem2lem2  49355  pgnbgreunbgrlem2lem3  49356  pgnbgreunbgrlem2  49357  pgnbgreunbgrlem4  49359  pgnbgreunbgrlem5  49363  upwlkbprop  49378  clcllaw  49430  intop  49442  assintop  49448  assintopcllaw  49451  elrngchomALTV  49508  rngccatidALTV  49511  rngcinvALTV  49515  rngcisoALTV  49516  rhmsubcALTVlem3  49522  rhmsubcALTVlem4  49523  funcringcsetcALTV2lem7  49535  elringchomALTV  49542  ringccatidALTV  49545  ringcisoALTV  49550  funcringcsetclem7ALTV  49558  prmringnzring  49576  ztprmneprm  49601  suppmptcfin  49630  linccl  49668  linc1  49679  lincolss  49688  ldepspr  49727  nn0sumshdiglem1  49875  0aryfvalelfv  49889  rrxlines  49988  rrxsphere  50002  itsclc0yqsol  50018  itschlc0xyqsol1  50020  fdomne0  50103  f002  50107  elovconstbrd  50117  fullthinc  50727