Theorem biimtrdi 254

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  ax12i  1973  sb4a  2488  hbsb2  2490  dfsb2  2501  2eu2  2656  reu6  3667  2reu2  3830  sseq0  4332  disjel  4386  disjpss  4390  preq12b  4782  prneimg  4786  preqsnd  4791  elinti  4887  zfrepclf  5214  exnelv  5236  dtruALT2  5300  opth1g  5419  sbcop1  5429  snopeqop  5448  propeqop  5449  otsndisj  5461  otiunsndisj  5462  iunopeqop  5463  iunopeqopOLD  5464  po2ne  5543  soasym  5560  elreldm  5878  dfres3  5937  relcnvtrg  6219  relresfld  6228  elpredimg  6268  ordtr2  6356  ordssun  6415  funopg  6520  funimass2  6569  f1imadifssran  6572  f0dom0  6712  elfv2ex  6871  fveqdmss  7020  eldmrexrnb  7034  fvcofneq  7035  funopsn  7091  funopsnOLD  7092  funopdmsn  7094  funsndifnop  7095  elunirn  7196  oprabidw  7388  oprabid  7389  brfvopab  7414  limuni3  7793  peano5  7834  resf1ext2b  7876  op1steq  7976  el2mpocsbcl  8025  bropopvvv  8030  bropfvvvv  8032  f1o2ndf1  8062  frxp  8067  fnwelem  8072  poxp2  8084  suppimacnv  8115  fvn0elsuppb  8122  suppfnss  8130  reldmtpos  8175  rntpos  8180  seqomlem2  8381  oaordi  8472  oa00  8485  oalimcl  8486  omeulem1  8508  nnaordi  8545  ecopovtrn  8758  undifixp  8873  mapdom2  9077  unxpdomlem3  9159  en1eqsn  9176  infssuni  9247  wdompwdom  9484  preleqg  9528  opthreg  9531  inf3lemd  9540  inf3lem2  9542  inf3lem6  9546  cnfcomlem  9612  cnfcom3  9617  karden  9811  carden2a  9882  alephdom  9995  dfac5lem4  10040  dfac5lem4OLD  10042  dfac12r  10061  kmlem2  10066  kmlem12  10076  cfslb2n  10182  alephsing  10190  fin23lem30  10256  fin1a2lem6  10319  fin1a2lem13  10326  axcc2lem  10350  domtriomlem  10356  axdc3lem2  10365  axdc4lem  10369  brdom6disj  10446  alephexp1  10494  pwfseq  10579  addnidpi  10816  indpi  10822  nqereu  10844  ltsonq  10884  distrlem5pr  10942  addcanpr  10961  suplem1pr  10967  suplem2pr  10968  ltsrpr  10992  ltsosr  11009  sqgt0sr  11021  leltne  11227  ltnsym  11236  ltlen  11239  eqlei  11248  eqlei2  11249  infm3  12107  nnunb  12425  0mnnnnn0  12461  elnnnn0b  12473  nn0ge2m1nn  12499  nn0le2is012  12585  btwnz  12624  uz11  12805  xrleltne  13088  xltnegi  13160  xnn0lenn0nn0  13189  xnn0xadd0  13191  xmulasslem2  13226  reltxrnmnf  13287  icogelb  13341  iccleub  13346  uznfz  13556  2ffzeq  13595  elfzonlteqm1  13688  elfzo0l  13703  fzoopth  13709  elfznelfzob  13721  elfzr  13728  elfzlmr  13729  injresinjlem  13737  injresinj  13738  fleqceilz  13805  modadd1  13859  modmul1  13878  modirr  13896  addmodlteq  13900  uzrdgfni  13912  fsuppmapnn0fiub0  13947  fsuppmapnn0ub  13949  seqf1o  13997  expnngt1  14195  hashrabsn01  14327  hashrabsn1  14328  hash1snb  14373  hash1n0  14375  hashf1lem2  14410  hash2prde  14424  hash2prd  14429  hash2pwpr  14430  hashle2pr  14431  hashle2prv  14432  hashge2el2dif  14434  hashge2el2difr  14435  hash3tpde  14447  fundmge2nop0  14456  ffz0iswrd  14495  ccatrcl1  14549  pfxsuff1eqwrdeq  14653  wrdind  14676  wrd2ind  14677  swrdccatin1  14679  swrdccat3blem  14693  2cshwcshw  14779  cshwcsh2id  14782  cshimadifsn  14783  2swrd2eqwrdeq  14907  wwlktovf  14910  wwlktovfo  14912  s3sndisj  14921  s3iunsndisj  14922  relexpindlem  15017  rexico  15308  lo1le  15606  fsum2dlem  15724  ntrivcvg  15854  fprodss  15905  fprod2dlem  15937  0dvds  16237  mod2eq1n2dvds  16308  opoe  16324  omoe  16325  opeo  16326  omeo  16327  m1exp1  16337  nn0enne  16338  nn0o1gt2  16342  gcdneg  16483  dfgcd2  16507  algcvga  16540  eucalglt  16546  lcmf  16594  coprmdvds  16614  divgcdcoprmex  16627  cncongr1  16628  prm2orodd  16652  prm23lt5  16777  pockthi  16870  prmreclem5  16883  ramtcl2  16974  cshwrepswhash1  17065  f1ocpbl  17481  f1ovscpbl  17482  f1olecpbl  17483  monhom  17694  epihom  17701  inveq  17733  invcoisoid  17751  isocoinvid  17752  ciclcl  17761  cicrcl  17762  isinitoi  17958  istermoi  17959  2initoinv  17969  2termoinv  17976  setciso  18050  embedsetcestrclem  18115  ipopos  18494  mgmpropd  18611  gsumval2a  18645  ismnddef  18696  dfgrp2e  18931  symg2bas  19360  snsymgefmndeq  19362  symgvalstruct  19364  symgfix2  19383  gsmsymgreq  19399  pmtrdifellem4  19446  mndodcongi  19510  pj1eu  19663  cycsubmcmn  19856  dprd2da  20011  rngimf1o  20426  rngimrnghm  20427  c0snmgmhm  20434  0ring01eq  20502  elrngchom  20597  rnghmsubcsetclem1  20604  rnghmsubcsetclem2  20605  rngcid  20608  rngcinv  20610  rngciso  20611  funcrngcsetcALT  20614  zrinitorngc  20615  zrtermorngc  20616  elringchom  20626  rhmsubcsetclem1  20633  rhmsubcsetclem2  20634  ringcid  20637  rhmsubcrngclem1  20639  rhmsubcrngclem2  20640  ringciso  20645  zrtermoringc  20648  rhmsubclem3  20660  rhmsubclem4  20661  lmodfopnelem1  20889  lspdisjb  21120  lspsnsubn0  21134  rngqiprngfulem2  21306  irinitoringc  21455  obs2ss  21705  mamufacex  22380  mat0dim0  22451  mat0dimid  22452  mat0dimscm  22453  dmatmat  22478  scmatmat  22493  mat1scmat  22523  1mavmul  22532  mavmulsolcl  22535  gsummatr01  22643  cpmatpmat  22694  cpmadugsumlemF  22860  tg2  22949  tgcl  22953  neii1  23090  neii2  23092  neindisj2  23107  perfopn  23169  ordtbas2  23175  pnfnei  23204  mnfnei  23205  llyidm  23472  txlm  23632  qtopuni  23686  tgqtop  23696  isfild  23842  snfil  23848  fbunfip  23853  fgss2  23858  fmco  23945  fbflim2  23961  cnpflf2  23984  fcfelbas  24020  fcfneii  24021  alexsubALTlem2  24032  alexsubALT  24035  tgpconncompeqg  24096  tsmscl  24119  tngngpim  24643  tgioo  24780  xrsmopn  24797  iccntr  24806  reconnlem2  24812  addcnlem  24849  htpycn  24959  phtpyhtpy  24968  pi1blem  25025  fgcfil  25257  ioombl1lem4  25547  dyadmbl  25586  itg2gt0  25746  ditgneg  25843  dvivthlem1  25994  coeeq2  26226  aannenlem2  26314  sineq0  26507  efif1o  26529  xrlimcnp  26951  vmacl  27100  efvmacl  27102  vmalelog  27187  dchrelbasd  27221  lgsqr  27333  lgsqrmodndvds  27335  gausslemma2dlem0i  27346  2lgslem2  27377  2lgs  27389  2lgsoddprmlem3  27396  2sqnn  27421  2sqreultlem  27429  2sqreultblem  27430  2sqreunnltlem  27432  2sqreunnltblem  27433  ltsintdifex  27644  ltsres  27645  nosepnelem  27662  nolt02o  27678  ltlesnd  27758  negsprop  28046  mulsprop  28141  onnolt  28277  onlts  28278  n0subs  28374  bdaypw2n0bndlem  28474  bdaypw2n0bnd  28475  bdayfinbndlem2  28479  elntg2  29073  uhgr0vb  29160  umgrupgr  29191  umgrnloopv  29194  umgredgprv  29195  umgrislfupgrlem  29210  umgredg  29226  uspgrushgr  29265  uspgrupgr  29266  usgruspgr  29268  usgredgprvALT  29283  usgrnloopvALT  29289  uhgr2edg  29296  edg0usgr  29341  egrsubgr  29365  0uhgrsubgr  29367  uhgrspansubgrlem  29378  nbuhgr  29431  cusgrsize2inds  29541  cusgrfilem2  29544  vtxdg0v  29561  1loopgrnb0  29590  vtxdginducedm1lem4  29630  wlkvtxeledg  29711  wlkeq  29721  wlkl1loop  29725  wlk1walk  29726  upgrwlkedg  29729  uspgr2wlkeq  29733  wlkv0  29737  wlkonl1iedg  29751  wlkon2n0  29752  wlkp1lem8  29766  wlkp1  29767  lfgrwlkprop  29773  lfgrwlknloop  29775  2pthnloop  29818  upgrwlkdvde  29824  spthonepeq  29839  uhgrwkspthlem2  29841  usgr2wlkneq  29843  usgr2trlncl  29847  usgr2trlspth  29848  pthdlem2lem  29854  clwlkcompbp  29869  uspgrn2crct  29895  wwlks  29922  wwlknbp  29929  0enwwlksnge1  29951  wwlkswwlksn  29952  wlklnwwlkln1  29955  wwlksnextproplem3  29998  wwlksnextprop  29999  wspthsnonn0vne  30004  wspn0  30011  2pthon3v  30030  umgr2adedgspth  30035  rusgr0edg  30063  clwwlkccat  30079  clwlkclwwlklem2fv2  30085  clwlkclwwlklem2a4  30086  clwlkclwwlklem2  30089  clwlkclwwlkflem  30093  clwwlknp  30126  clwwlkwwlksb  30143  clwwlkext2edg  30145  erclwwlkneqlen  30157  hashecclwwlkn1  30166  umgrhashecclwwlk  30167  clwwlknonwwlknonb  30195  upgr1wlkdlem1  30234  upgr3v3e3cycl  30269  uhgr3cyclexlem  30270  1conngr  30283  conngrv2edg  30284  eupth2lem3lem4  30320  eulercrct  30331  isfrgr  30349  frgr3vlem2  30363  1to2vfriswmgr  30368  1to3vfriswmgr  30369  frgrncvvdeqlem9  30396  frgrwopreg  30412  frgr2wwlkeqm  30420  2wspmdisj  30426  numclwwlk1lem2f  30444  frgrreggt1  30482  frgrregord013  30484  frgrregord13  30485  l2p  30569  nmlno0lem  30883  normgt0  31217  ocin  31386  nmlnop0iALT  32085  nmopun  32104  cvpss  32375  cvnbtwn  32376  atcvati  32476  mdsymlem6  32498  iunrnmptss  32655  expgt0b  32910  wrdt2ind  33033  irngssv  33881  issgon  34316  mbfmcnt  34461  ballotlemfc0  34686  ballotlemfcc  34687  satfv0  35595  satfv0fun  35608  fmla1  35624  gonarlem  35631  gonar  35632  goalrlem  35633  goalr  35634  fmla0disjsuc  35635  satffunlem  35638  satffunlem1lem1  35639  satffunlem2lem1  35641  satfun  35648  satfv0fvfmla0  35650  sategoelfv  35657  mthmblem  35817  pprodss4v  36119  funpartfun  36180  funpartfv  36182  5segofs  36243  btwnxfr  36293  brofs2  36314  brifs2  36315  btwnconn1  36338  segleantisym  36352  broutsideof2  36359  outsidene1  36360  outsidene2  36361  funray  36377  lineunray  36384  cldbnd  36563  bj-imdirval3  37553  topdifinffinlem  37718  isbasisrelowllem1  37726  isbasisrelowllem2  37727  relowlpssretop  37735  inunissunidif  37746  pibt2  37788  matunitlindf  37994  poimir  38029  volsupnfl  38041  itg2addnclem  38047  cover2  38091  sdclem2  38118  fdc  38121  sstotbnd3  38152  heibor1  38186  clmgmOLD  38227  smgrpmgm  38240  smgrpassOLD  38241  dvrunz  38330  0rngo  38403  mopickr  38747  sucmapleftuniq  38866  lsatcvat  39551  lshpkrex  39619  cmtbr3N  39755  atn0  39809  atnle  39818  cvlsupr4  39846  cvlsupr5  39847  cvlsupr6  39848  cvrval4N  39915  cvratlem  39922  2llnjN  40068  2lplnj  40121  linepsubN  40253  elpaddatiN  40306  elpcliN  40394  pclcmpatN  40402  ldilval  40614  ltrnu  40622  cdleme18d  40796  tendotp  41262  tendof  41264  tendovalco  41266  diatrl  41545  diaintclN  41559  dvheveccl  41613  dibintclN  41668  dihord6apre  41757  dihmeetlem1N  41791  dihpN  41837  dihintcl  41845  dochkrshp4  41890  oexpreposd  42808  pw2f1ocnv  43491  iocinico  43666  onsucf1olem  43724  succlg  43782  oacl2g  43784  omabs2  43786  omcl2  43787  naddcnfcom  43820  naddcnfass  43823  safesnsupfidom1o  43870  infordmin  43985  pr2cv  44001  expgrowthi  44786  iotavalsb  44886  bi23imp1  44948  ioogtlb  45948  iocgtlb  45955  iocleub  45956  icoltub  45961  iooltub  45963  stoweidlem31  46482  oppr  47501  funressnfv  47514  fsetsniunop  47520  fsetsnf1  47523  eu2ndop1stv  47596  afvelrnb0  47635  otiunsndisjX  47750  el1fzopredsuc  47797  2ffzoeq  47799  uniimaprimaeqfv  47865  elsetpreimafveqfv  47875  iccpartimp  47900  iccpartrn  47913  iccpartf  47914  iccpartnel  47921  fargshiftf  47923  fargshiftfo  47925  ichnfimlem  47946  ichnfim  47947  ichreuopeq  47956  sprel  47967  sprsymrelfvlem  47973  sprsymrelfolem2  47976  prproropf1olem4  47989  prprelb  47999  poprelb  48007  fmtnofac1  48056  prmdvdsfmtnof1lem2  48071  31prm  48083  lighneallem3  48093  ppivalnnnprm  48114  nn0o1gt2ALTV  48193  nn0oALTV  48195  odd2prm2  48217  mogoldbblem  48219  fpprbasnn  48228  fpprnn  48229  sbgoldbaltlem1  48278  nnsum3primesle9  48293  bgoldbtbndlem1  48304  bgoldbtbndlem2  48305  grimedgi  48435  grtriproplem  48438  grtriprop  48440  cycl3grtrilem  48445  cycl3grtri  48446  isubgr3stgrlem8  48472  gpgvtxel2  48547  gpgedgiov  48564  gpgedg2iv  48566  gpgprismgr4cycllem7  48600  pgnbgreunbgrlem1  48612  pgnbgreunbgrlem2lem1  48613  pgnbgreunbgrlem2lem2  48614  pgnbgreunbgrlem2lem3  48615  pgnbgreunbgrlem2  48616  pgnbgreunbgrlem4  48618  pgnbgreunbgrlem5  48622  upwlkbprop  48637  clcllaw  48690  intop  48702  assintop  48708  assintopcllaw  48711  elrngchomALTV  48768  rngccatidALTV  48771  rngcinvALTV  48775  rngcisoALTV  48776  rhmsubcALTVlem3  48782  rhmsubcALTVlem4  48783  funcringcsetcALTV2lem7  48795  elringchomALTV  48802  ringccatidALTV  48805  ringcisoALTV  48810  funcringcsetclem7ALTV  48818  ztprmneprm  48846  suppmptcfin  48875  linccl  48913  linc1  48924  lincolss  48933  ldepspr  48972  nn0sumshdiglem1  49120  0aryfvalelfv  49134  rrxlines  49232  rrxsphere  49247  itsclc0yqsol  49263  itschlc0xyqsol1  49265  fdomne0  49348  f002  49352  fvconstr2  49362  fullthinc  49948