Theorem biimtrdi 253

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 229	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  ax12i  1966  sb4a  2484  hbsb2  2486  dfsb2  2497  2eu2  2652  reu6  3709  2reu2  3873  sseq0  4378  disjel  4432  disjpss  4436  preq12b  4826  prneimg  4830  preqsnd  4835  elinti  4931  zfrepclf  5261  dtruALT2  5340  dtruOLD  5416  opth1g  5453  sbcop1  5463  snopeqop  5481  propeqop  5482  otsndisj  5494  otiunsndisj  5495  iunopeqop  5496  po2ne  5577  soasym  5594  elreldm  5915  dfres3  5971  relcnvtrg  6255  relresfld  6265  elpredimg  6305  ordtr2  6397  ordssun  6455  funopg  6569  funimass2  6618  f1imadifssran  6621  f0dom0  6761  elfv2ex  6921  fveqdmss  7067  eldmrexrnb  7081  fvcofneq  7082  funopsn  7137  funopdmsn  7139  funsndifnop  7140  elunirn  7242  oprabidw  7434  oprabid  7435  brfvopab  7462  limuni3  7845  peano5  7887  resf1ext2b  7929  op1steq  8030  el2mpocsbcl  8082  bropopvvv  8087  bropfvvvv  8089  f1o2ndf1  8119  frxp  8123  fnwelem  8128  poxp2  8140  suppimacnv  8171  fvn0elsuppb  8178  suppfnss  8186  reldmtpos  8231  rntpos  8236  seqomlem2  8463  oaordi  8556  oa00  8569  oalimcl  8570  omeulem1  8592  nnaordi  8628  ecopovtrn  8832  undifixp  8946  mapdom2  9160  unxpdomlem3  9258  en1eqsn  9278  enp1iOLD  9284  infssuni  9356  wdompwdom  9590  preleqg  9627  opthreg  9630  inf3lemd  9639  inf3lem2  9641  inf3lem6  9645  cnfcomlem  9711  cnfcom3  9716  karden  9907  carden2a  9978  alephdom  10093  dfac5lem4  10138  dfac5lem4OLD  10140  dfac12r  10159  kmlem2  10164  kmlem12  10174  cfslb2n  10280  alephsing  10288  fin23lem30  10354  fin1a2lem6  10417  fin1a2lem13  10424  axcc2lem  10448  domtriomlem  10454  axdc3lem2  10463  axdc4lem  10467  brdom6disj  10544  alephexp1  10591  pwfseq  10676  addnidpi  10913  indpi  10919  nqereu  10941  ltsonq  10981  distrlem5pr  11039  addcanpr  11058  suplem1pr  11064  suplem2pr  11065  ltsrpr  11089  ltsosr  11106  sqgt0sr  11118  leltne  11322  ltnsym  11331  ltlen  11334  eqlei  11343  eqlei2  11344  infm3  12199  nnunb  12495  0mnnnnn0  12531  elnnnn0b  12543  nn0ge2m1nn  12569  nn0le2is012  12655  btwnz  12694  uz11  12875  xrleltne  13159  xltnegi  13230  xnn0lenn0nn0  13259  xnn0xadd0  13261  xmulasslem2  13296  reltxrnmnf  13357  icogelb  13411  iccleub  13416  uznfz  13625  2ffzeq  13664  elfzonlteqm1  13755  elfzo0l  13770  fzoopth  13776  elfznelfzob  13787  elfzr  13794  elfzlmr  13795  injresinjlem  13801  injresinj  13802  fleqceilz  13869  modadd1  13923  modmul1  13940  modirr  13958  addmodlteq  13962  uzrdgfni  13974  fsuppmapnn0fiub0  14009  fsuppmapnn0ub  14011  seqf1o  14059  expnngt1  14257  hashrabsn01  14389  hashrabsn1  14390  hash1snb  14435  hash1n0  14437  hashf1lem2  14472  hash2prde  14486  hash2prd  14491  hash2pwpr  14492  hashle2pr  14493  hashle2prv  14494  hashge2el2dif  14496  hashge2el2difr  14497  hash3tpde  14509  fundmge2nop0  14518  ffz0iswrd  14557  ccatrcl1  14610  pfxsuff1eqwrdeq  14715  wrdind  14738  wrd2ind  14739  swrdccatin1  14741  swrdccat3blem  14755  2cshwcshw  14842  cshwcsh2id  14845  cshimadifsn  14846  2swrd2eqwrdeq  14970  wwlktovf  14973  wwlktovfo  14975  s3sndisj  14984  s3iunsndisj  14985  relexpindlem  15080  rexico  15370  lo1le  15666  fsum2dlem  15784  ntrivcvg  15911  fprodss  15962  fprod2dlem  15994  0dvds  16294  mod2eq1n2dvds  16364  opoe  16380  omoe  16381  opeo  16382  omeo  16383  m1exp1  16393  nn0enne  16394  nn0o1gt2  16398  gcdneg  16539  dfgcd2  16563  algcvga  16596  eucalglt  16602  lcmf  16650  coprmdvds  16670  divgcdcoprmex  16683  cncongr1  16684  prm2orodd  16708  prm23lt5  16832  pockthi  16925  prmreclem5  16938  ramtcl2  17029  cshwrepswhash1  17120  f1ocpbl  17537  f1ovscpbl  17538  f1olecpbl  17539  monhom  17746  epihom  17753  inveq  17785  invcoisoid  17803  isocoinvid  17804  ciclcl  17813  cicrcl  17814  isinitoi  18010  istermoi  18011  2initoinv  18021  2termoinv  18028  setciso  18102  embedsetcestrclem  18167  ipopos  18544  mgmpropd  18627  gsumval2a  18661  ismnddef  18712  dfgrp2e  18944  symg2bas  19372  snsymgefmndeq  19374  symgvalstruct  19376  symgfix2  19395  gsmsymgreq  19411  pmtrdifellem4  19458  mndodcongi  19522  pj1eu  19675  cycsubmcmn  19868  dprd2da  20023  rngimf1o  20412  rngimrnghm  20413  c0snmgmhm  20420  0ring01eq  20487  elrngchom  20582  rnghmsubcsetclem1  20589  rnghmsubcsetclem2  20590  rngcid  20593  rngcinv  20595  rngciso  20596  funcrngcsetcALT  20599  zrinitorngc  20600  zrtermorngc  20601  elringchom  20611  rhmsubcsetclem1  20618  rhmsubcsetclem2  20619  ringcid  20622  rhmsubcrngclem1  20624  rhmsubcrngclem2  20625  ringciso  20630  zrtermoringc  20633  rhmsubclem3  20645  rhmsubclem4  20646  lmodfopnelem1  20853  lspdisjb  21085  lspsnsubn0  21099  rngqiprngfulem2  21271  irinitoringc  21438  obs2ss  21687  mamufacex  22332  mat0dim0  22403  mat0dimid  22404  mat0dimscm  22405  dmatmat  22430  scmatmat  22445  mat1scmat  22475  1mavmul  22484  mavmulsolcl  22487  gsummatr01  22595  cpmatpmat  22646  cpmadugsumlemF  22812  tg2  22901  tgcl  22905  neii1  23042  neii2  23044  neindisj2  23059  perfopn  23121  ordtbas2  23127  pnfnei  23156  mnfnei  23157  llyidm  23424  txlm  23584  qtopuni  23638  tgqtop  23648  isfild  23794  snfil  23800  fbunfip  23805  fgss2  23810  fmco  23897  fbflim2  23913  cnpflf2  23936  fcfelbas  23972  fcfneii  23973  alexsubALTlem2  23984  alexsubALT  23987  tgpconncompeqg  24048  tsmscl  24071  tngngpim  24596  tgioo  24733  xrsmopn  24750  iccntr  24759  reconnlem2  24765  addcnlem  24802  htpycn  24921  phtpyhtpy  24930  pi1blem  24988  fgcfil  25221  ioombl1lem4  25512  dyadmbl  25551  itg2gt0  25711  ditgneg  25808  dvivthlem1  25963  coeeq2  26197  aannenlem2  26287  sineq0  26483  efif1o  26505  xrlimcnp  26928  vmacl  27078  efvmacl  27080  vmalelog  27166  dchrelbasd  27200  lgsqr  27312  lgsqrmodndvds  27314  gausslemma2dlem0i  27325  2lgslem2  27356  2lgs  27368  2lgsoddprmlem3  27375  2sqnn  27400  2sqreultlem  27408  2sqreultblem  27409  2sqreunnltlem  27411  2sqreunnltblem  27412  sltintdifex  27623  sltres  27624  nosepnelem  27641  nolt02o  27657  sltlend  27733  negsprop  27984  mulsprop  28073  n0subs  28277  elntg2  28910  uhgr0vb  28997  umgrupgr  29028  umgrnloopv  29031  umgredgprv  29032  umgrislfupgrlem  29047  umgredg  29063  uspgrushgr  29102  uspgrupgr  29103  usgruspgr  29105  usgredgprvALT  29120  usgrnloopvALT  29126  uhgr2edg  29133  edg0usgr  29178  egrsubgr  29202  0uhgrsubgr  29204  uhgrspansubgrlem  29215  nbuhgr  29268  cusgrsize2inds  29379  cusgrfilem2  29382  vtxdg0v  29399  1loopgrnb0  29428  vtxdginducedm1lem4  29468  wlkvtxeledg  29550  wlkeq  29560  wlkl1loop  29564  wlk1walk  29565  upgrwlkedg  29568  uspgr2wlkeq  29572  wlkv0  29577  wlkonl1iedg  29591  wlkon2n0  29592  wlkp1lem8  29606  wlkp1  29607  lfgrwlkprop  29613  lfgrwlknloop  29615  2pthnloop  29659  upgrwlkdvde  29665  spthonepeq  29680  uhgrwkspthlem2  29682  usgr2wlkneq  29684  usgr2trlncl  29688  usgr2trlspth  29689  pthdlem2lem  29695  clwlkcompbp  29710  uspgrn2crct  29736  wwlks  29763  wwlknbp  29770  0enwwlksnge1  29792  wwlkswwlksn  29793  wlklnwwlkln1  29796  wwlksnextproplem3  29839  wwlksnextprop  29840  wspthsnonn0vne  29845  wspn0  29852  2pthon3v  29871  umgr2adedgspth  29876  rusgr0edg  29901  clwwlkccat  29917  clwlkclwwlklem2fv2  29923  clwlkclwwlklem2a4  29924  clwlkclwwlklem2  29927  clwlkclwwlkflem  29931  clwwlknp  29964  clwwlkwwlksb  29981  clwwlkext2edg  29983  erclwwlkneqlen  29995  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwwlknonwwlknonb  30033  upgr1wlkdlem1  30072  upgr3v3e3cycl  30107  uhgr3cyclexlem  30108  1conngr  30121  conngrv2edg  30122  eupth2lem3lem4  30158  eulercrct  30169  isfrgr  30187  frgr3vlem2  30201  1to2vfriswmgr  30206  1to3vfriswmgr  30207  frgrncvvdeqlem9  30234  frgrwopreg  30250  frgr2wwlkeqm  30258  2wspmdisj  30264  numclwwlk1lem2f  30282  frgrreggt1  30320  frgrregord013  30322  frgrregord13  30323  l2p  30406  nmlno0lem  30720  normgt0  31054  ocin  31223  nmlnop0iALT  31922  nmopun  31941  cvpss  32212  cvnbtwn  32213  atcvati  32313  mdsymlem6  32335  iunrnmptss  32492  expgt0b  32741  wrdt2ind  32875  irngssv  33675  issgon  34100  mbfmcnt  34246  ballotlemfc0  34471  ballotlemfcc  34472  satfv0  35326  satfv0fun  35339  fmla1  35355  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  fmla0disjsuc  35366  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  satfun  35379  satfv0fvfmla0  35381  sategoelfv  35388  mthmblem  35548  pprodss4v  35848  funpartfun  35907  funpartfv  35909  5segofs  35970  btwnxfr  36020  brofs2  36041  brifs2  36042  btwnconn1  36065  segleantisym  36079  broutsideof2  36086  outsidene1  36087  outsidene2  36088  funray  36104  lineunray  36111  cldbnd  36290  bj-imdirval3  37148  topdifinffinlem  37311  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlpssretop  37328  inunissunidif  37339  pibt2  37381  matunitlindf  37588  poimir  37623  volsupnfl  37635  itg2addnclem  37641  cover2  37685  sdclem2  37712  fdc  37715  sstotbnd3  37746  heibor1  37780  clmgmOLD  37821  smgrpmgm  37834  smgrpassOLD  37835  dvrunz  37924  0rngo  37997  mopickr  38327  lsatcvat  39014  lshpkrex  39082  cmtbr3N  39218  atn0  39272  atnle  39281  cvlsupr4  39309  cvlsupr5  39310  cvlsupr6  39311  cvrval4N  39379  cvratlem  39386  2llnjN  39532  2lplnj  39585  linepsubN  39717  elpaddatiN  39770  elpcliN  39858  pclcmpatN  39866  ldilval  40078  ltrnu  40086  cdleme18d  40260  tendotp  40726  tendof  40728  tendovalco  40730  diatrl  41009  diaintclN  41023  dvheveccl  41077  dibintclN  41132  dihord6apre  41221  dihmeetlem1N  41255  dihpN  41301  dihintcl  41309  dochkrshp4  41354  oexpreposd  42318  pw2f1ocnv  43008  iocinico  43183  onsucf1olem  43241  succlg  43299  oacl2g  43301  omabs2  43303  omcl2  43304  naddcnfcom  43337  naddcnfass  43340  safesnsupfidom1o  43388  infordmin  43503  pr2cv  43519  expgrowthi  44305  iotavalsb  44405  bi23imp1  44468  ioogtlb  45472  iocgtlb  45479  iocleub  45480  icoltub  45485  iooltub  45487  stoweidlem31  46008  oppr  47007  funressnfv  47020  fsetsniunop  47026  fsetsnf1  47029  eu2ndop1stv  47102  afvelrnb0  47141  otiunsndisjX  47256  el1fzopredsuc  47302  2ffzoeq  47304  uniimaprimaeqfv  47344  elsetpreimafveqfv  47354  iccpartimp  47379  iccpartrn  47392  iccpartf  47393  iccpartnel  47400  fargshiftf  47402  fargshiftfo  47404  ichnfimlem  47425  ichnfim  47426  ichreuopeq  47435  sprel  47446  sprsymrelfvlem  47452  sprsymrelfolem2  47455  prproropf1olem4  47468  prprelb  47478  poprelb  47486  fmtnofac1  47532  prmdvdsfmtnof1lem2  47547  31prm  47559  lighneallem3  47569  nn0o1gt2ALTV  47656  nn0oALTV  47658  odd2prm2  47680  mogoldbblem  47682  fpprbasnn  47691  fpprnn  47692  sbgoldbaltlem1  47741  nnsum3primesle9  47756  bgoldbtbndlem1  47767  bgoldbtbndlem2  47768  grtriproplem  47899  grtriprop  47901  cycl3grtrilem  47906  cycl3grtri  47907  isubgr3stgrlem8  47933  gpgvtxel2  48000  gpgprismgr4cycllem7  48048  upwlkbprop  48061  clcllaw  48114  intop  48126  assintop  48132  assintopcllaw  48135  elrngchomALTV  48192  rngccatidALTV  48195  rngcinvALTV  48199  rngcisoALTV  48200  rhmsubcALTVlem3  48206  rhmsubcALTVlem4  48207  funcringcsetcALTV2lem7  48219  elringchomALTV  48226  ringccatidALTV  48229  ringcisoALTV  48234  funcringcsetclem7ALTV  48242  ztprmneprm  48270  suppmptcfin  48299  linccl  48338  linc1  48349  lincolss  48358  ldepspr  48397  nn0sumshdiglem1  48549  0aryfvalelfv  48563  rrxlines  48661  rrxsphere  48676  itsclc0yqsol  48692  itschlc0xyqsol1  48694  fdomne0  48776  f002  48780  fvconstr2  48788  fullthinc  49284