Theorem biimtrrid 246

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)

Hypotheses

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

Assertion

Ref	Expression
biimtrrid	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem biimtrrid

Step	Hyp	Ref	Expression
1		biimtrrid.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 231	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 35	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:  3imtr3g  298  oplem1  1072  nic-ax  1706  19.30  1914  19.33b  1918  sbrimvw  2128  necon1bd  2973  rexlimdvvva  3220  spc2d  3556  pssdifn0  4316  ralnralall  4469  disjss3  5102  somo  5602  frminex  5634  sofld  6180  predtrss  6320  ordelord  6379  unizlim  6482  f0rn0  6761  funopfv  6928  mpteqb  7007  fvrnressn  7159  funfvima  7230  fpropnf1  7265  fliftfun  7314  weniso  7358  tfinds  7857  tfindsg  7858  tfindes  7860  tfinds2  7861  findsg  7895  resf1ext2b  7933  frxp  8125  poxp2  8142  soseq  8158  suppssr  8194  rdgsucmptnf  8419  frsucmptn  8429  tz7.49  8435  om00  8563  oewordi  8580  iiner  8790  eroveu  8813  fsetexb  8866  sdomdif  9124  pssnn  9164  sucdom2  9198  php3  9204  unxpdomlem3  9229  fisseneq  9234  ordunifi  9261  isfinite2  9269  fiint  9297  infssuni  9314  ixpfi2  9318  finsschain  9327  ordtypelem10  9500  wofib  9518  wemapsolem  9523  unxpwdom2  9561  inf3lem2  9609  cantnfp1lem3  9660  cantnfp1  9661  setind  9727  frr3g  9739  r1tr  9759  r1ordg  9761  rankelb  9807  rankxplim3  9864  updjudhf  9937  cardlim  9978  infxpenlem  10017  infxpenc2  10026  dfac5lem4  10130  dfac12k  10151  kmlem13  10166  sornom  10280  fin23lem25  10327  fin23lem21  10342  zorn2lem4  10502  iundom2g  10549  fpwwe2lem11  10651  fpwwe2lem12  10652  pwfseqlem4a  10671  eltsk2g  10761  inttsk  10784  tskord  10790  r1tskina  10792  grudomon  10827  arch  12526  zaddcl  12659  uzm1  12922  xrsupsslem  13360  xrinfmsslem  13361  fsequb  14040  fseqsupubi  14043  ssnn0fi  14050  seqf1o  14108  sq01  14290  ccatalpha  14661  swrdnd0  14728  repsdf2  14850  cshw1  14894  wrdl3s3  15036  rexanre  15435  rexuzre  15441  cau3lem  15443  o1co  15674  rlimcn3  15678  o1of2  15701  lo1add  15715  lo1mul  15716  climcau  15759  climbdd  15760  caucvgb  15768  summo  15804  isumltss  15938  mertenslem2  15975  prodmolem2  16023  prodmo  16024  dvdsaddre2b  16398  bitsfzolem  16525  bitsfzo  16526  bezoutlem4  16633  lcmfeq0b  16721  lcmfunsnlem2  16731  divgcdcoprmex  16757  prmind2  16776  2mulprm  16784  isprm5  16799  prmdvdsbc  16818  prm23ge5  16908  pcqmul  16946  pcadd  16982  prmreclem2  17010  prmreclem5  17013  mul4sq  17047  vdwmc2  17072  ramcl  17122  prmgaplem7  17150  prmlem1a  17199  setsstruct2  17267  divsfval  17634  iscatd2  17770  catpropd  17798  wunfunc  17991  cyccom  19332  gaorber  19436  psgneu  19634  lsmsubm  19781  pj1eu  19824  efgredlem  19875  qusabl  19993  cygctb  20020  lt6abl  20023  gsumval3eu  20032  dprdsubg  20154  ablfac1c  20201  pgpfac1  20210  dvdsrtr  20510  unitgrp  20525  abvn0b  21003  lvecvs0or  21296  lspdisjb  21314  lspsolvlem  21330  lspprat  21341  lbsextlem2  21347  nzerooringczr  21694  domnchr  21746  znfld  21774  cygznlem3  21783  obselocv  21942  lindsenlbs  22065  cpmatacl  22942  chfacfisf  23080  chfacfisfcpmat  23081  0ntr  23297  opnneiid  23352  restntr  23408  hausnei2  23579  nrmsep3  23581  cmpsub  23626  uncmp  23629  dfconn2  23645  cnconn  23648  1stcfb  23671  txuni2  23792  txbas  23794  ptbasin  23804  txcls  23831  txbasval  23833  txlly  23863  txnlly  23864  pthaus  23865  txlm  23875  tx1stc  23877  xkohaus  23880  isufil2  24135  ufileu  24146  cnpflfi  24226  txflf  24233  fclscf  24252  flimfnfcls  24255  alexsubb  24273  alexsubALTlem2  24275  alexsubALTlem4  24277  ptcmplem2  24280  ptcmplem3  24281  cnextcn  24294  qustgplem  24348  prdsmet  24597  blin2  24656  prdsbl  24718  nmolb  24944  tgqioo  25027  reconnlem2  25055  reconn  25056  lebnumlem3  25192  iscau4  25508  cmetcaulem  25517  iscmet3lem2  25521  bcthlem5  25557  minveclem3b  25657  pmltpc  25679  evthicc2  25689  ovolunlem2  25727  ovolicc2lem5  25750  mblsplit  25761  iundisj2  25778  volsup  25785  ioombl1lem4  25790  dyaddisj  25825  dyadmbllem  25828  i1faddlem  25922  itg10a  25939  itg1ge0a  25940  mbfi1flimlem  25951  mbfmullem  25954  itg2add  25988  rolle  26218  dvcvx  26248  itgsubst  26277  tdeglem4  26286  ply1domn  26350  fta1b  26398  plyadd  26444  plymul  26445  coeeu  26452  vieta1  26545  aalioulem6  26574  ulmcaulem  26631  ulmcau  26632  ulmbdd  26635  ulmcn  26636  amgm  27228  mumullem2  27417  ppiublem1  27439  dchrfi  27492  dchrptlem2  27502  dchrptlem3  27503  dchrsum2  27505  lgsdchr  27592  lgsquad2lem2  27622  2sqlem5  27659  2sqb  27669  pntlemp  27847  ostthlem2  27865  ostth  27876  nosupprefixmo  27937  noinfprefixmo  27938  noetasuplem4  27973  madebdaylemlrcut  28165  addsproplem2  28236  precsexlem11  28483  ltonold  28527  bdayfinbndlem1  28733  iscgrglt  28857  tgbtwnconn1  28918  colline  28998  lmimid  29179  axcontlem8  29429  axcontlem9  29430  eengtrkg  29444  numedglnl  29602  uhgr2edg  29669  uspgr2wlkeq  30106  wlkonl1iedg  30124  wlkdlem2  30142  pthdlem2  30234  clwlkclwwlklem2a4  30468  clwwisshclwwsn  30487  clwwlknon1sn  30571  frgr2wwlkeu  30808  frgrreg  30875  frgrregord013  30876  nvmul0or  31132  ubthlem3  31354  axhcompl-zf  31480  hvmul0or  31507  ocnel  31780  pjhthmo  31784  spanuni  32026  spansni  32039  hon0  32275  leopadd  32614  leoptr  32619  mdsymlem6  32890  sumdmdlem2  32901  cdjreui  32914  iundisj2f  33064  disjunsn  33068  iundisj2fi  33269  ballotlemimin  35018  bnj23  35229  bnj594  35422  bnj849  35435  setindregs  35657  karddom  35688  kardsdom  35689  cusgr3cyclex  35726  txsconn  35821  cvmsdisj  35850  cvmliftlem15  35878  cvmlift2lem10  35892  cvmlift3lem7  35905  fmla1  35967  satffunlem1lem2  35983  satffunlem2lem2  35986  mclsppslem  36163  dfon2lem3  36363  dfon2lem5  36365  dfon2lem6  36366  dfon2lem7  36367  dfon2lem8  36368  ifscgr  36625  cgr3tr4  36633  btwnconn1lem13  36680  seglecgr12  36692  elicc3  36937  neibastop1  36979  tailfb  36997  bj-sblem2  37587  bj-sngltag  37728  copsex2d  37892  mptsnunlem  38093  finxpreclem6  38151  wl-equsal1i  38308  poimirlem26  38396  poimirlem27  38397  ismblfin  38411  itg2addnclem3  38423  ftc1anclem6  38448  fdc  38496  riscer  38739  intidl  38780  ispridlc  38821  disjlem14  39650  disjlem17  39651  prtlem14  39748  prtlem17  39750  lpssat  39887  lssatle  39889  lshpkrlem6  39989  cvrnbtwn  40145  atlatmstc  40193  atlatle  40194  atlrelat1  40195  2at0mat0  40399  trlator0  41045  cdleme0moN  41099  cdlemn11pre  42084  dihord2pre  42099  dihmeetlem20N  42200  dochkrshp4  42263  lcfl6  42374  expeqidd  43201  remullid  43310  diophin  43618  diophun  43619  inaex  45122  pm10.57  45196  modelaxreplem1  45802  fnchoice  45864  ellimcabssub0  46448  fourierdlem81  47016  fourierdlem93  47028  2reuimp0  48003  fzopredsuc  48213  2ffzoeq  48217  m1modmmod  48253  iccpartlt  48325  ichnreuop  48373  prmdvdsfmtnof1lem1  48488  lighneallem4  48514  odd2prm2  48635  even3prm2  48636  sbgoldbst  48695  nnsum4primesevenALTV  48718  stgrvtx0  48879  isubgr3stgrlem6  48888  grlimprclnbgrvtx  48916  pgnbgreunbgr  49042  ply1mulgsumlem1  49317  snlindsntor  49402  islininds2  49415  itschlc0xyqsol1  49697  2itscp  49712  opnneir  49834  iscnrm3lem2  49862