Theorem biimtrrid 244

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 229	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	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:  3imtr3g  296  oplem1  1062  nic-ax  1680  19.30  1888  19.33b  1892  necon1bd  2952  rexlimdvvva  3197  spc2d  3540  pssdifn0  4296  ralnralall  4441  disjss3  5071  somo  5565  frminex  5597  sofld  6138  predtrss  6273  ordelord  6332  unizlim  6434  f0rn0  6712  funopfv  6876  mpteqb  6955  fvrnressn  7104  funfvima  7174  fpropnf1  7211  fliftfun  7256  weniso  7298  tfinds  7800  tfindsg  7801  tfindes  7803  tfinds2  7804  findsg  7837  resf1ext2b  7875  frxp  8066  poxp2  8083  soseq  8099  suppssr  8135  rdgsucmptnf  8358  frsucmptn  8368  tz7.49  8374  om00  8500  oewordi  8517  iiner  8726  eroveu  8749  fsetexb  8801  sdomdif  9053  pssnn  9093  sucdom2  9127  php3  9133  unxpdomlem3  9158  fisseneq  9163  ordunifi  9190  isfinite2  9198  fiint  9227  infssuni  9246  ixpfi2  9250  finsschain  9259  ordtypelem10  9432  wofib  9450  wemapsolem  9455  unxpwdom2  9493  inf3lem2  9541  cantnfp1lem3  9592  cantnfp1  9593  setind  9659  frr3g  9671  r1tr  9691  r1ordg  9693  rankelb  9739  rankxplim3  9796  updjudhf  9846  cardlim  9887  infxpenlem  9926  infxpenc2  9935  dfac5lem4  10039  dfac5lem4OLD  10041  dfac12k  10061  kmlem13  10076  sornom  10190  fin23lem25  10237  fin23lem21  10252  zorn2lem4  10412  iundom2g  10453  fpwwe2lem11  10555  fpwwe2lem12  10556  pwfseqlem4a  10575  eltsk2g  10665  inttsk  10688  tskord  10694  r1tskina  10696  grudomon  10731  arch  12425  zaddcl  12558  uzm1  12813  xrsupsslem  13250  xrinfmsslem  13251  fsequb  13928  fseqsupubi  13931  ssnn0fi  13938  seqf1o  13996  sq01  14178  ccatalpha  14547  swrdnd0  14611  repsdf2  14731  cshw1  14775  wrdl3s3  14915  rexanre  15300  rexuzre  15306  cau3lem  15308  o1co  15539  rlimcn3  15543  o1of2  15566  lo1add  15580  lo1mul  15581  climcau  15624  climbdd  15625  caucvgb  15633  summo  15670  isumltss  15804  mertenslem2  15841  prodmolem2  15891  prodmo  15892  dvdsaddre2b  16267  bitsfzolem  16394  bitsfzo  16395  bezoutlem4  16502  lcmfeq0b  16590  lcmfunsnlem2  16600  divgcdcoprmex  16626  prmind2  16645  2mulprm  16653  isprm5  16668  prmdvdsbc  16687  prm23ge5  16777  pcqmul  16815  pcadd  16851  prmreclem2  16879  prmreclem5  16882  mul4sq  16916  vdwmc2  16941  ramcl  16991  prmgaplem7  17019  prmlem1a  17068  setsstruct2  17135  divsfval  17502  iscatd2  17638  catpropd  17666  wunfunc  17859  cyccom  19169  gaorber  19274  psgneu  19472  lsmsubm  19619  pj1eu  19662  efgredlem  19713  qusabl  19831  cygctb  19858  lt6abl  19861  gsumval3eu  19870  dprdsubg  19992  ablfac1c  20039  pgpfac1  20048  dvdsrtr  20339  unitgrp  20354  drngmul0orOLD  20733  abvn0b  20808  lvecvs0or  21101  lspdisjb  21119  lspsolvlem  21135  lspprat  21146  lbsextlem2  21152  nzerooringczr  21455  domnchr  21507  znfld  21535  cygznlem3  21544  obselocv  21703  cpmatacl  22699  chfacfisf  22837  chfacfisfcpmat  22838  0ntr  23054  opnneiid  23109  restntr  23165  hausnei2  23336  nrmsep3  23338  cmpsub  23383  uncmp  23386  dfconn2  23402  cnconn  23405  1stcfb  23428  txuni2  23548  txbas  23550  ptbasin  23560  txcls  23587  txbasval  23589  txlly  23619  txnlly  23620  pthaus  23621  txlm  23631  tx1stc  23633  xkohaus  23636  isufil2  23891  ufileu  23902  cnpflfi  23982  txflf  23989  fclscf  24008  flimfnfcls  24011  alexsubb  24029  alexsubALTlem2  24031  alexsubALTlem4  24033  ptcmplem2  24036  ptcmplem3  24037  cnextcn  24050  qustgplem  24104  prdsmet  24353  blin2  24412  prdsbl  24474  nmolb  24700  tgqioo  24783  reconnlem2  24811  reconn  24812  lebnumlem3  24948  iscau4  25264  cmetcaulem  25273  iscmet3lem2  25277  bcthlem5  25313  minveclem3b  25413  pmltpc  25435  evthicc2  25445  ovolunlem2  25483  ovolicc2lem5  25506  mblsplit  25517  iundisj2  25534  volsup  25541  ioombl1lem4  25546  dyaddisj  25581  dyadmbllem  25584  i1faddlem  25678  itg10a  25695  itg1ge0a  25696  mbfi1flimlem  25707  mbfmullem  25710  itg2add  25744  rolle  25975  dvcvx  26005  itgsubst  26034  tdeglem4  26043  ply1domn  26107  fta1b  26155  plyadd  26200  plymul  26201  coeeu  26208  vieta1  26296  aalioulem6  26321  ulmcaulem  26377  ulmcau  26378  ulmbdd  26381  ulmcn  26382  amgm  26972  mumullem2  27161  ppiublem1  27183  dchrfi  27236  dchrptlem2  27246  dchrptlem3  27247  dchrsum2  27249  lgsdchr  27336  lgsquad2lem2  27366  2sqlem5  27403  2sqb  27413  pntlemp  27591  ostthlem2  27609  ostth  27620  nosupprefixmo  27682  noinfprefixmo  27683  noetasuplem4  27718  madebdaylemlrcut  27909  addsproplem2  27980  precsexlem11  28227  ltonold  28271  bdayfinbndlem1  28477  iscgrglt  28600  tgbtwnconn1  28661  colline  28735  lmimid  28880  axcontlem8  29058  axcontlem9  29059  eengtrkg  29073  numedglnl  29231  uhgr2edg  29295  uspgr2wlkeq  29732  wlkonl1iedg  29750  wlkdlem2  29768  pthdlem2  29854  clwlkclwwlklem2a4  30085  clwwisshclwwsn  30104  clwwlknon1sn  30188  frgr2wwlkeu  30415  frgrreg  30482  frgrregord013  30483  nvmul0or  30739  ubthlem3  30961  axhcompl-zf  31087  hvmul0or  31114  ocnel  31387  pjhthmo  31391  spanuni  31633  spansni  31646  hon0  31882  leopadd  32221  leoptr  32226  mdsymlem6  32497  sumdmdlem2  32508  cdjreui  32521  iundisj2f  32679  disjunsn  32683  iundisj2fi  32889  ballotlemimin  34690  bnj23  34901  bnj594  35094  bnj849  35107  setindregs  35311  cusgr3cyclex  35364  txsconn  35469  cvmsdisj  35498  cvmliftlem15  35526  cvmlift2lem10  35540  cvmlift3lem7  35553  fmla1  35615  satffunlem1lem2  35631  satffunlem2lem2  35634  mclsppslem  35811  dfon2lem3  36011  dfon2lem5  36013  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  ifscgr  36272  cgr3tr4  36280  btwnconn1lem13  36327  seglecgr12  36339  elicc3  36545  neibastop1  36587  tailfb  36605  bj-sblem2  37196  bj-sngltag  37336  copsex2d  37499  mptsnunlem  37700  finxpreclem6  37758  wl-equsal1i  37915  lindsenlbs  37982  poimirlem26  38013  poimirlem27  38014  ismblfin  38028  itg2addnclem3  38040  ftc1anclem6  38065  fdc  38112  riscer  38355  intidl  38396  ispridlc  38437  disjlem14  39268  disjlem17  39269  prtlem14  39366  prtlem17  39368  lpssat  39505  lssatle  39507  lshpkrlem6  39607  cvrnbtwn  39763  atlatmstc  39811  atlatle  39812  atlrelat1  39813  2at0mat0  40017  trlator0  40663  cdleme0moN  40717  cdlemn11pre  41702  dihord2pre  41717  dihmeetlem20N  41818  dochkrshp4  41881  lcfl6  41992  expeqidd  42802  remullid  42911  diophin  43221  diophun  43222  inaex  44741  pm10.57  44815  modelaxreplem1  45422  fnchoice  45477  ellimcabssub0  46062  fourierdlem81  46630  fourierdlem93  46642  2reuimp0  47577  fzopredsuc  47787  2ffzoeq  47791  m1modmmod  47827  iccpartlt  47899  ichnreuop  47947  prmdvdsfmtnof1lem1  48062  lighneallem4  48088  odd2prm2  48209  even3prm2  48210  sbgoldbst  48269  nnsum4primesevenALTV  48292  stgrvtx0  48453  isubgr3stgrlem6  48462  grlimprclnbgrvtx  48490  pgnbgreunbgr  48616  ply1mulgsumlem1  48877  snlindsntor  48962  islininds2  48975  itschlc0xyqsol1  49257  2itscp  49272  opnneir  49397  iscnrm3lem2  49425