Theorem biimtrrid 245

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 230	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3g  297  oplem1  1068  nic-ax  1693  19.30  1901  19.33b  1905  sbrimvw  2124  necon1bd  2975  rexlimdvvva  3220  spc2d  3561  pssdifn0  4321  ralnralall  4467  disjss3  5099  somo  5594  frminex  5626  sofld  6173  predtrss  6309  ordelord  6368  unizlim  6470  f0rn0  6749  funopfv  6916  mpteqb  6995  fvrnressn  7144  funfvima  7214  fpropnf1  7251  fliftfun  7296  weniso  7338  tfinds  7840  tfindsg  7841  tfindes  7843  tfinds2  7844  findsg  7878  resf1ext2b  7916  frxp  8106  poxp2  8123  soseq  8139  suppssr  8175  rdgsucmptnf  8400  frsucmptn  8410  tz7.49  8416  om00  8544  oewordi  8561  iiner  8771  eroveu  8794  fsetexb  8845  sdomdif  9097  pssnn  9137  sucdom2  9171  php3  9177  unxpdomlem3  9202  fisseneq  9207  ordunifi  9234  isfinite2  9242  fiint  9271  infssuni  9289  ixpfi2  9293  finsschain  9302  ordtypelem10  9475  wofib  9493  wemapsolem  9498  unxpwdom2  9536  inf3lem2  9584  cantnfp1lem3  9635  cantnfp1  9636  setind  9702  frr3g  9714  r1tr  9734  r1ordg  9736  rankelb  9782  rankxplim3  9839  updjudhf  9889  cardlim  9930  infxpenlem  9969  infxpenc2  9978  dfac5lem4  10082  dfac5lem4OLD  10084  dfac12k  10104  kmlem13  10119  sornom  10234  fin23lem25  10281  fin23lem21  10296  zorn2lem4  10456  iundom2g  10497  fpwwe2lem11  10599  fpwwe2lem12  10600  pwfseqlem4a  10619  eltsk2g  10709  inttsk  10732  tskord  10738  r1tskina  10740  grudomon  10775  arch  12478  zaddcl  12611  uzm1  12873  xrsupsslem  13310  xrinfmsslem  13311  fsequb  13988  fseqsupubi  13991  ssnn0fi  13998  seqf1o  14056  sq01  14238  ccatalpha  14607  swrdnd0  14671  repsdf2  14791  cshw1  14835  wrdl3s3  14975  rexanre  15374  rexuzre  15380  cau3lem  15382  o1co  15613  rlimcn3  15617  o1of2  15640  lo1add  15654  lo1mul  15655  climcau  15698  climbdd  15699  caucvgb  15707  summo  15744  isumltss  15878  mertenslem2  15915  prodmolem2  15965  prodmo  15966  dvdsaddre2b  16341  bitsfzolem  16468  bitsfzo  16469  bezoutlem4  16576  lcmfeq0b  16664  lcmfunsnlem2  16674  divgcdcoprmex  16700  prmind2  16719  2mulprm  16727  isprm5  16742  prmdvdsbc  16761  prm23ge5  16851  pcqmul  16889  pcadd  16925  prmreclem2  16953  prmreclem5  16956  mul4sq  16990  vdwmc2  17015  ramcl  17065  prmgaplem7  17093  prmlem1a  17142  setsstruct2  17210  divsfval  17577  iscatd2  17713  catpropd  17741  wunfunc  17934  cyccom  19244  gaorber  19348  psgneu  19546  lsmsubm  19693  pj1eu  19736  efgredlem  19787  qusabl  19905  cygctb  19932  lt6abl  19935  gsumval3eu  19944  dprdsubg  20066  ablfac1c  20113  pgpfac1  20122  dvdsrtr  20417  unitgrp  20432  drngmul0orOLD  20811  abvn0b  20885  lvecvs0or  21178  lspdisjb  21196  lspsolvlem  21212  lspprat  21223  lbsextlem2  21229  nzerooringczr  21532  domnchr  21584  znfld  21612  cygznlem3  21621  obselocv  21780  cpmatacl  22776  chfacfisf  22914  chfacfisfcpmat  22915  0ntr  23131  opnneiid  23186  restntr  23242  hausnei2  23413  nrmsep3  23415  cmpsub  23460  uncmp  23463  dfconn2  23479  cnconn  23482  1stcfb  23505  txuni2  23625  txbas  23627  ptbasin  23637  txcls  23664  txbasval  23666  txlly  23696  txnlly  23697  pthaus  23698  txlm  23708  tx1stc  23710  xkohaus  23713  isufil2  23968  ufileu  23979  cnpflfi  24059  txflf  24066  fclscf  24085  flimfnfcls  24088  alexsubb  24106  alexsubALTlem2  24108  alexsubALTlem4  24110  ptcmplem2  24113  ptcmplem3  24114  cnextcn  24127  qustgplem  24181  prdsmet  24430  blin2  24489  prdsbl  24551  nmolb  24777  tgqioo  24860  reconnlem2  24888  reconn  24889  lebnumlem3  25025  iscau4  25341  cmetcaulem  25350  iscmet3lem2  25354  bcthlem5  25390  minveclem3b  25490  pmltpc  25512  evthicc2  25522  ovolunlem2  25560  ovolicc2lem5  25583  mblsplit  25594  iundisj2  25611  volsup  25618  ioombl1lem4  25623  dyaddisj  25658  dyadmbllem  25661  i1faddlem  25755  itg10a  25772  itg1ge0a  25773  mbfi1flimlem  25784  mbfmullem  25787  itg2add  25821  rolle  26052  dvcvx  26082  itgsubst  26111  tdeglem4  26120  ply1domn  26184  fta1b  26232  plyadd  26277  plymul  26278  coeeu  26285  vieta1  26376  aalioulem6  26401  ulmcaulem  26457  ulmcau  26458  ulmbdd  26461  ulmcn  26462  amgm  27055  mumullem2  27244  ppiublem1  27266  dchrfi  27319  dchrptlem2  27329  dchrptlem3  27330  dchrsum2  27332  lgsdchr  27419  lgsquad2lem2  27449  2sqlem5  27486  2sqb  27496  pntlemp  27674  ostthlem2  27692  ostth  27703  nosupprefixmo  27764  noinfprefixmo  27765  noetasuplem4  27800  madebdaylemlrcut  27992  addsproplem2  28063  precsexlem11  28310  ltonold  28354  bdayfinbndlem1  28560  iscgrglt  28683  tgbtwnconn1  28744  colline  28819  lmimid  28967  axcontlem8  29172  axcontlem9  29173  eengtrkg  29187  numedglnl  29345  uhgr2edg  29409  uspgr2wlkeq  29846  wlkonl1iedg  29864  wlkdlem2  29882  pthdlem2  29968  clwlkclwwlklem2a4  30199  clwwisshclwwsn  30218  clwwlknon1sn  30302  frgr2wwlkeu  30529  frgrreg  30596  frgrregord013  30597  nvmul0or  30853  ubthlem3  31075  axhcompl-zf  31201  hvmul0or  31228  ocnel  31501  pjhthmo  31505  spanuni  31747  spansni  31760  hon0  31996  leopadd  32335  leoptr  32340  mdsymlem6  32611  sumdmdlem2  32622  cdjreui  32635  iundisj2f  32790  disjunsn  32794  iundisj2fi  32999  ballotlemimin  34803  bnj23  35014  bnj594  35207  bnj849  35220  setindregs  35426  cusgr3cyclex  35486  txsconn  35591  cvmsdisj  35620  cvmliftlem15  35648  cvmlift2lem10  35662  cvmlift3lem7  35675  fmla1  35737  satffunlem1lem2  35753  satffunlem2lem2  35756  mclsppslem  35933  dfon2lem3  36133  dfon2lem5  36135  dfon2lem6  36136  dfon2lem7  36137  dfon2lem8  36138  ifscgr  36394  cgr3tr4  36402  btwnconn1lem13  36449  seglecgr12  36461  elicc3  36677  neibastop1  36719  tailfb  36737  bj-sblem2  37328  bj-sngltag  37468  copsex2d  37631  mptsnunlem  37832  finxpreclem6  37890  wl-equsal1i  38047  lindsenlbs  38114  poimirlem26  38145  poimirlem27  38146  ismblfin  38160  itg2addnclem3  38172  ftc1anclem6  38197  fdc  38244  riscer  38487  intidl  38528  ispridlc  38569  disjlem14  39400  disjlem17  39401  prtlem14  39498  prtlem17  39500  lpssat  39637  lssatle  39639  lshpkrlem6  39739  cvrnbtwn  39895  atlatmstc  39943  atlatle  39944  atlrelat1  39945  2at0mat0  40149  trlator0  40795  cdleme0moN  40849  cdlemn11pre  41834  dihord2pre  41849  dihmeetlem20N  41950  dochkrshp4  42013  lcfl6  42124  expeqidd  42934  remullid  43043  diophin  43353  diophun  43354  inaex  44873  pm10.57  44947  modelaxreplem1  45554  fnchoice  45609  ellimcabssub0  46193  fourierdlem81  46761  fourierdlem93  46773  2reuimp0  47708  fzopredsuc  47918  2ffzoeq  47922  m1modmmod  47958  iccpartlt  48030  ichnreuop  48078  prmdvdsfmtnof1lem1  48193  lighneallem4  48219  odd2prm2  48340  even3prm2  48341  sbgoldbst  48400  nnsum4primesevenALTV  48423  stgrvtx0  48584  isubgr3stgrlem6  48593  grlimprclnbgrvtx  48621  pgnbgreunbgr  48747  ply1mulgsumlem1  49008  snlindsntor  49093  islininds2  49106  itschlc0xyqsol1  49388  2itscp  49403  opnneir  49528  iscnrm3lem2  49556