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  1056  nic-ax  1673  19.30  1881  19.33b  1885  necon1bd  2943  rexlimdvvva  3195  spc2d  3568  pssdifn0  4331  ralnralall  4478  disjss3  5106  somo  5585  frminex  5617  sofld  6160  predtrss  6295  ordelord  6354  unizlim  6457  f0rn0  6745  funopfv  6910  mpteqb  6987  fvrnressn  7133  funfvima  7204  fpropnf1  7242  fliftfun  7287  weniso  7329  tfinds  7836  tfindsg  7837  tfindes  7839  tfinds2  7840  findsg  7873  resf1ext2b  7911  frxp  8105  poxp2  8122  soseq  8138  suppssr  8174  rdgsucmptnf  8397  frsucmptn  8407  tz7.49  8413  om00  8539  oewordi  8555  iiner  8762  eroveu  8785  fsetexb  8837  sdomdif  9089  pssnn  9132  sucdom2  9167  php3  9173  unxpdomlem3  9199  fisseneq  9204  ordunifi  9237  isfinite2  9245  fiint  9277  fiintOLD  9278  infssuni  9297  ixpfi2  9301  finsschain  9310  ordtypelem10  9480  wofib  9498  wemapsolem  9503  unxpwdom2  9541  inf3lem2  9582  cantnfp1lem3  9633  cantnfp1  9634  setind  9687  frr3g  9709  r1tr  9729  r1ordg  9731  rankelb  9777  rankxplim3  9834  updjudhf  9884  cardlim  9925  infxpenlem  9966  infxpenc2  9975  dfac5lem4  10079  dfac5lem4OLD  10081  dfac12k  10101  kmlem13  10116  sornom  10230  fin23lem25  10277  fin23lem21  10292  zorn2lem4  10452  iundom2g  10493  fpwwe2lem11  10594  fpwwe2lem12  10595  pwfseqlem4a  10614  eltsk2g  10704  inttsk  10727  tskord  10733  r1tskina  10735  grudomon  10770  arch  12439  zaddcl  12573  uzm1  12831  xrsupsslem  13267  xrinfmsslem  13268  fsequb  13940  fseqsupubi  13943  ssnn0fi  13950  seqf1o  14008  sq01  14190  ccatalpha  14558  swrdnd0  14622  repsdf2  14743  cshw1  14787  wrdl3s3  14928  rexanre  15313  rexuzre  15319  cau3lem  15321  o1co  15552  rlimcn3  15556  o1of2  15579  lo1add  15593  lo1mul  15594  climcau  15637  climbdd  15638  caucvgb  15646  summo  15683  isumltss  15814  mertenslem2  15851  prodmolem2  15901  prodmo  15902  dvdsaddre2b  16277  bitsfzolem  16404  bitsfzo  16405  bezoutlem4  16512  lcmfeq0b  16600  lcmfunsnlem2  16610  divgcdcoprmex  16636  prmind2  16655  2mulprm  16663  isprm5  16677  prmdvdsbc  16696  prm23ge5  16786  pcqmul  16824  pcadd  16860  prmreclem2  16888  prmreclem5  16891  mul4sq  16925  vdwmc2  16950  ramcl  17000  prmgaplem7  17028  prmlem1a  17077  setsstruct2  17144  divsfval  17510  iscatd2  17642  catpropd  17670  wunfunc  17863  cyccom  19135  gaorber  19240  psgneu  19436  lsmsubm  19583  pj1eu  19626  efgredlem  19677  qusabl  19795  cygctb  19822  lt6abl  19825  gsumval3eu  19834  dprdsubg  19956  ablfac1c  20003  pgpfac1  20012  dvdsrtr  20277  unitgrp  20292  drngmul0orOLD  20670  abvn0b  20745  lvecvs0or  21018  lspdisjb  21036  lspsolvlem  21052  lspprat  21063  lbsextlem2  21069  nzerooringczr  21390  domnchr  21442  znfld  21470  cygznlem3  21479  obselocv  21637  cpmatacl  22603  chfacfisf  22741  chfacfisfcpmat  22742  0ntr  22958  opnneiid  23013  restntr  23069  hausnei2  23240  nrmsep3  23242  cmpsub  23287  uncmp  23290  dfconn2  23306  cnconn  23309  1stcfb  23332  txuni2  23452  txbas  23454  ptbasin  23464  txcls  23491  txbasval  23493  txlly  23523  txnlly  23524  pthaus  23525  txlm  23535  tx1stc  23537  xkohaus  23540  isufil2  23795  ufileu  23806  cnpflfi  23886  txflf  23893  fclscf  23912  flimfnfcls  23915  alexsubb  23933  alexsubALTlem2  23935  alexsubALTlem4  23937  ptcmplem2  23940  ptcmplem3  23941  cnextcn  23954  qustgplem  24008  prdsmet  24258  blin2  24317  prdsbl  24379  nmolb  24605  tgqioo  24688  reconnlem2  24716  reconn  24717  lebnumlem3  24862  iscau4  25179  cmetcaulem  25188  iscmet3lem2  25192  bcthlem5  25228  minveclem3b  25328  pmltpc  25351  evthicc2  25361  ovolunlem2  25399  ovolicc2lem5  25422  mblsplit  25433  iundisj2  25450  volsup  25457  ioombl1lem4  25462  dyaddisj  25497  dyadmbllem  25500  i1faddlem  25594  itg10a  25611  itg1ge0a  25612  mbfi1flimlem  25623  mbfmullem  25626  itg2add  25660  rolle  25894  dvcvx  25925  itgsubst  25956  tdeglem4  25965  ply1domn  26029  fta1b  26077  plyadd  26122  plymul  26123  coeeu  26130  vieta1  26220  aalioulem6  26245  ulmcaulem  26303  ulmcau  26304  ulmbdd  26307  ulmcn  26308  amgm  26901  mumullem2  27090  ppiublem1  27113  dchrfi  27166  dchrptlem2  27176  dchrptlem3  27177  dchrsum2  27179  lgsdchr  27266  lgsquad2lem2  27296  2sqlem5  27333  2sqb  27343  pntlemp  27521  ostthlem2  27539  ostth  27550  nosupprefixmo  27612  noinfprefixmo  27613  noetasuplem4  27648  madebdaylemlrcut  27810  addsproplem2  27877  precsexlem11  28119  sltonold  28162  iscgrglt  28441  tgbtwnconn1  28502  colline  28576  lmimid  28721  axcontlem8  28898  axcontlem9  28899  eengtrkg  28913  numedglnl  29071  uhgr2edg  29135  uspgr2wlkeq  29574  wlkonl1iedg  29593  wlkdlem2  29611  pthdlem2  29698  clwlkclwwlklem2a4  29926  clwwisshclwwsn  29945  clwwlknon1sn  30029  frgr2wwlkeu  30256  frgrreg  30323  frgrregord013  30324  nvmul0or  30579  ubthlem3  30801  axhcompl-zf  30927  hvmul0or  30954  ocnel  31227  pjhthmo  31231  spanuni  31473  spansni  31486  hon0  31722  leopadd  32061  leoptr  32066  mdsymlem6  32337  sumdmdlem2  32348  cdjreui  32361  iundisj2f  32519  disjunsn  32523  iundisj2fi  32720  ballotlemimin  34497  bnj23  34708  bnj594  34902  bnj849  34915  cusgr3cyclex  35123  txsconn  35228  cvmsdisj  35257  cvmliftlem15  35285  cvmlift2lem10  35299  cvmlift3lem7  35312  fmla1  35374  satffunlem1lem2  35390  satffunlem2lem2  35393  mclsppslem  35570  dfon2lem3  35773  dfon2lem5  35775  dfon2lem6  35776  dfon2lem7  35777  dfon2lem8  35778  ifscgr  36032  cgr3tr4  36040  btwnconn1lem13  36087  seglecgr12  36099  elicc3  36305  neibastop1  36347  tailfb  36365  bj-sblem2  36831  bj-sngltag  36971  copsex2d  37127  mptsnunlem  37326  finxpreclem6  37384  wl-equsal1i  37532  lindsenlbs  37609  poimirlem26  37640  poimirlem27  37641  ismblfin  37655  itg2addnclem3  37667  ftc1anclem6  37692  fdc  37739  riscer  37982  intidl  38023  ispridlc  38064  disjlem14  38790  disjlem17  38791  prtlem14  38867  prtlem17  38869  lpssat  39006  lssatle  39008  lshpkrlem6  39108  cvrnbtwn  39264  atlatmstc  39312  atlatle  39313  atlrelat1  39314  2at0mat0  39519  trlator0  40165  cdleme0moN  40219  cdlemn11pre  41204  dihord2pre  41219  dihmeetlem20N  41320  dochkrshp4  41383  lcfl6  41494  expeqidd  42313  remullid  42422  diophin  42760  diophun  42761  inaex  44286  pm10.57  44360  modelaxreplem1  44968  fnchoice  45023  ellimcabssub0  45615  fourierdlem81  46185  fourierdlem93  46197  2reuimp0  47115  fzopredsuc  47324  2ffzoeq  47328  m1modmmod  47359  iccpartlt  47425  ichnreuop  47473  prmdvdsfmtnof1lem1  47585  lighneallem4  47611  odd2prm2  47719  even3prm2  47720  sbgoldbst  47779  nnsum4primesevenALTV  47802  stgrvtx0  47961  isubgr3stgrlem6  47970  pgnbgreunbgr  48115  ply1mulgsumlem1  48375  snlindsntor  48460  islininds2  48473  itschlc0xyqsol1  48755  2itscp  48770  opnneir  48895  iscnrm3lem2  48923