Theorem biimtrrid 243

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 228	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	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:  3imtr3g  295  oplem1  1057  nic-ax  1671  19.30  1880  19.33b  1884  necon1bd  2964  rexlimdvvva  3220  spc2d  3615  pssdifn0  4391  ralnralall  4538  disjss3  5165  somo  5646  frminex  5679  sofld  6218  predtrss  6354  ordelord  6417  unizlim  6518  f0rn0  6806  funopfv  6972  mpteqb  7048  fvrnressn  7195  funfvima  7267  fpropnf1  7304  fliftfun  7348  weniso  7390  tfinds  7897  tfindsg  7898  tfindes  7900  tfinds2  7901  findsg  7937  frxp  8167  poxp2  8184  soseq  8200  suppssr  8236  rdgsucmptnf  8485  frsucmptn  8495  tz7.49  8501  om00  8631  oewordi  8647  iiner  8847  eroveu  8870  fsetexb  8922  undomOLD  9126  sucdom2OLD  9148  sdomdif  9191  pssnn  9234  sucdom2  9269  php3  9275  php3OLD  9287  unxpdomlem3  9315  fisseneq  9320  ordunifi  9354  isfinite2  9362  fiint  9394  fiintOLD  9395  infssuni  9414  ixpfi2  9420  finsschain  9429  ordtypelem10  9596  wofib  9614  wemapsolem  9619  unxpwdom2  9657  inf3lem2  9698  cantnfp1lem3  9749  cantnfp1  9750  setind  9803  frr3g  9825  r1tr  9845  r1ordg  9847  rankelb  9893  rankxplim3  9950  updjudhf  10000  cardlim  10041  infxpenlem  10082  infxpenc2  10091  dfac5lem4  10195  dfac5lem4OLD  10197  dfac12k  10217  kmlem13  10232  sornom  10346  fin23lem25  10393  fin23lem21  10408  zorn2lem4  10568  iundom2g  10609  fpwwe2lem11  10710  fpwwe2lem12  10711  pwfseqlem4a  10730  eltsk2g  10820  inttsk  10843  tskord  10849  r1tskina  10851  grudomon  10886  arch  12550  zaddcl  12683  uzm1  12941  xrsupsslem  13369  xrinfmsslem  13370  fsequb  14026  fseqsupubi  14029  ssnn0fi  14036  seqf1o  14094  sq01  14274  ccatalpha  14641  swrdnd0  14705  repsdf2  14826  cshw1  14870  wrdl3s3  15011  rexanre  15395  rexuzre  15401  cau3lem  15403  o1co  15632  rlimcn3  15636  o1of2  15659  lo1add  15673  lo1mul  15674  climcau  15719  climbdd  15720  caucvgb  15728  summo  15765  isumltss  15896  mertenslem2  15933  prodmolem2  15983  prodmo  15984  dvdsaddre2b  16355  bitsfzolem  16480  bitsfzo  16481  bezoutlem4  16589  lcmfeq0b  16677  lcmfunsnlem2  16687  divgcdcoprmex  16713  prmind2  16732  2mulprm  16740  isprm5  16754  prmdvdsbc  16773  prm23ge5  16862  pcqmul  16900  pcadd  16936  prmreclem2  16964  prmreclem5  16967  mul4sq  17001  vdwmc2  17026  ramcl  17076  prmgaplem7  17104  prmlem1a  17154  setsstruct2  17221  divsfval  17607  iscatd2  17739  catpropd  17767  wunfunc  17965  wunfuncOLD  17966  cyccom  19243  gaorber  19348  psgneu  19548  lsmsubm  19695  pj1eu  19738  efgredlem  19789  qusabl  19907  cygctb  19934  lt6abl  19937  gsumval3eu  19946  dprdsubg  20068  ablfac1c  20115  pgpfac1  20124  dvdsrtr  20394  unitgrp  20409  drngmul0orOLD  20783  abvn0b  20859  lvecvs0or  21133  lspdisjb  21151  lspsolvlem  21167  lspprat  21178  lbsextlem2  21184  nzerooringczr  21514  domnchr  21570  znfld  21602  cygznlem3  21611  obselocv  21771  cpmatacl  22743  chfacfisf  22881  chfacfisfcpmat  22882  0ntr  23100  opnneiid  23155  restntr  23211  hausnei2  23382  nrmsep3  23384  cmpsub  23429  uncmp  23432  dfconn2  23448  cnconn  23451  1stcfb  23474  txuni2  23594  txbas  23596  ptbasin  23606  txcls  23633  txbasval  23635  txlly  23665  txnlly  23666  pthaus  23667  txlm  23677  tx1stc  23679  xkohaus  23682  isufil2  23937  ufileu  23948  cnpflfi  24028  txflf  24035  fclscf  24054  flimfnfcls  24057  alexsubb  24075  alexsubALTlem2  24077  alexsubALTlem4  24079  ptcmplem2  24082  ptcmplem3  24083  cnextcn  24096  qustgplem  24150  prdsmet  24401  blin2  24460  prdsbl  24525  nmolb  24759  tgqioo  24841  reconnlem2  24868  reconn  24869  lebnumlem3  25014  iscau4  25332  cmetcaulem  25341  iscmet3lem2  25345  bcthlem5  25381  minveclem3b  25481  pmltpc  25504  evthicc2  25514  ovolunlem2  25552  ovolicc2lem5  25575  mblsplit  25586  iundisj2  25603  volsup  25610  ioombl1lem4  25615  dyaddisj  25650  dyadmbllem  25653  i1faddlem  25747  itg10a  25765  itg1ge0a  25766  mbfi1flimlem  25777  mbfmullem  25780  itg2add  25814  rolle  26048  dvcvx  26079  itgsubst  26110  tdeglem4  26119  ply1domn  26183  fta1b  26231  plyadd  26276  plymul  26277  coeeu  26284  vieta1  26372  aalioulem6  26397  ulmcaulem  26455  ulmcau  26456  ulmbdd  26459  ulmcn  26460  amgm  27052  mumullem2  27241  ppiublem1  27264  dchrfi  27317  dchrptlem2  27327  dchrptlem3  27328  dchrsum2  27330  lgsdchr  27417  lgsquad2lem2  27447  2sqlem5  27484  2sqb  27494  pntlemp  27672  ostthlem2  27690  ostth  27701  nosupprefixmo  27763  noinfprefixmo  27764  noetasuplem4  27799  madebdaylemlrcut  27955  addsproplem2  28021  precsexlem11  28259  sltonold  28301  iscgrglt  28540  tgbtwnconn1  28601  colline  28675  lmimid  28820  axcontlem8  29004  axcontlem9  29005  eengtrkg  29019  numedglnl  29179  uhgr2edg  29243  uspgr2wlkeq  29682  wlkonl1iedg  29701  wlkdlem2  29719  pthdlem2  29804  clwlkclwwlklem2a4  30029  clwwisshclwwsn  30048  clwwlknon1sn  30132  frgr2wwlkeu  30359  frgrreg  30426  frgrregord013  30427  nvmul0or  30682  ubthlem3  30904  axhcompl-zf  31030  hvmul0or  31057  ocnel  31330  pjhthmo  31334  spanuni  31576  spansni  31589  hon0  31825  leopadd  32164  leoptr  32169  mdsymlem6  32440  sumdmdlem2  32451  cdjreui  32464  iundisj2f  32612  disjunsn  32616  iundisj2fi  32802  ballotlemimin  34470  bnj23  34694  bnj594  34888  bnj849  34901  cusgr3cyclex  35104  txsconn  35209  cvmsdisj  35238  cvmliftlem15  35266  cvmlift2lem10  35280  cvmlift3lem7  35293  fmla1  35355  satffunlem1lem2  35371  satffunlem2lem2  35374  mclsppslem  35551  dfon2lem3  35749  dfon2lem5  35751  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  ifscgr  36008  cgr3tr4  36016  btwnconn1lem13  36063  seglecgr12  36075  elicc3  36283  neibastop1  36325  tailfb  36343  bj-sblem2  36809  bj-sngltag  36949  copsex2d  37105  mptsnunlem  37304  finxpreclem6  37362  wl-equsal1i  37498  lindsenlbs  37575  poimirlem26  37606  poimirlem27  37607  ismblfin  37621  itg2addnclem3  37633  ftc1anclem6  37658  fdc  37705  riscer  37948  intidl  37989  ispridlc  38030  disjlem14  38754  disjlem17  38755  prtlem14  38830  prtlem17  38832  lpssat  38969  lssatle  38971  lshpkrlem6  39071  cvrnbtwn  39227  atlatmstc  39275  atlatle  39276  atlrelat1  39277  2at0mat0  39482  trlator0  40128  cdleme0moN  40182  cdlemn11pre  41167  dihord2pre  41182  dihmeetlem20N  41283  dochkrshp4  41346  lcfl6  41457  expeqidd  42312  remullid  42409  diophin  42728  diophun  42729  inaex  44266  pm10.57  44340  fnchoice  44929  ellimcabssub0  45538  fourierdlem81  46108  fourierdlem93  46120  2reuimp0  47029  fzopredsuc  47238  2ffzoeq  47242  iccpartlt  47298  ichnreuop  47346  prmdvdsfmtnof1lem1  47458  lighneallem4  47484  odd2prm2  47592  even3prm2  47593  sbgoldbst  47652  nnsum4primesevenALTV  47675  ply1mulgsumlem1  48115  snlindsntor  48200  islininds2  48213  m1modmmod  48255  itschlc0xyqsol1  48500  2itscp  48515  opnneir  48586  iscnrm3lem2  48614