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  3193  spc2d  3565  pssdifn0  4327  ralnralall  4474  disjss3  5101  somo  5578  frminex  5610  sofld  6148  predtrss  6283  ordelord  6342  unizlim  6445  f0rn0  6727  funopfv  6892  mpteqb  6969  fvrnressn  7115  funfvima  7186  fpropnf1  7224  fliftfun  7269  weniso  7311  tfinds  7816  tfindsg  7817  tfindes  7819  tfinds2  7820  findsg  7853  resf1ext2b  7891  frxp  8082  poxp2  8099  soseq  8115  suppssr  8151  rdgsucmptnf  8374  frsucmptn  8384  tz7.49  8390  om00  8516  oewordi  8532  iiner  8739  eroveu  8762  fsetexb  8814  sdomdif  9066  pssnn  9109  sucdom2  9144  php3  9150  unxpdomlem3  9175  fisseneq  9180  ordunifi  9213  isfinite2  9221  fiint  9253  fiintOLD  9254  infssuni  9273  ixpfi2  9277  finsschain  9286  ordtypelem10  9456  wofib  9474  wemapsolem  9479  unxpwdom2  9517  inf3lem2  9558  cantnfp1lem3  9609  cantnfp1  9610  setind  9663  frr3g  9685  r1tr  9705  r1ordg  9707  rankelb  9753  rankxplim3  9810  updjudhf  9860  cardlim  9901  infxpenlem  9942  infxpenc2  9951  dfac5lem4  10055  dfac5lem4OLD  10057  dfac12k  10077  kmlem13  10092  sornom  10206  fin23lem25  10253  fin23lem21  10268  zorn2lem4  10428  iundom2g  10469  fpwwe2lem11  10570  fpwwe2lem12  10571  pwfseqlem4a  10590  eltsk2g  10680  inttsk  10703  tskord  10709  r1tskina  10711  grudomon  10746  arch  12415  zaddcl  12549  uzm1  12807  xrsupsslem  13243  xrinfmsslem  13244  fsequb  13916  fseqsupubi  13919  ssnn0fi  13926  seqf1o  13984  sq01  14166  ccatalpha  14534  swrdnd0  14598  repsdf2  14719  cshw1  14763  wrdl3s3  14904  rexanre  15289  rexuzre  15295  cau3lem  15297  o1co  15528  rlimcn3  15532  o1of2  15555  lo1add  15569  lo1mul  15570  climcau  15613  climbdd  15614  caucvgb  15622  summo  15659  isumltss  15790  mertenslem2  15827  prodmolem2  15877  prodmo  15878  dvdsaddre2b  16253  bitsfzolem  16380  bitsfzo  16381  bezoutlem4  16488  lcmfeq0b  16576  lcmfunsnlem2  16586  divgcdcoprmex  16612  prmind2  16631  2mulprm  16639  isprm5  16653  prmdvdsbc  16672  prm23ge5  16762  pcqmul  16800  pcadd  16836  prmreclem2  16864  prmreclem5  16867  mul4sq  16901  vdwmc2  16926  ramcl  16976  prmgaplem7  17004  prmlem1a  17053  setsstruct2  17120  divsfval  17486  iscatd2  17618  catpropd  17646  wunfunc  17839  cyccom  19111  gaorber  19216  psgneu  19412  lsmsubm  19559  pj1eu  19602  efgredlem  19653  qusabl  19771  cygctb  19798  lt6abl  19801  gsumval3eu  19810  dprdsubg  19932  ablfac1c  19979  pgpfac1  19988  dvdsrtr  20253  unitgrp  20268  drngmul0orOLD  20646  abvn0b  20721  lvecvs0or  20994  lspdisjb  21012  lspsolvlem  21028  lspprat  21039  lbsextlem2  21045  nzerooringczr  21366  domnchr  21418  znfld  21446  cygznlem3  21455  obselocv  21613  cpmatacl  22579  chfacfisf  22717  chfacfisfcpmat  22718  0ntr  22934  opnneiid  22989  restntr  23045  hausnei2  23216  nrmsep3  23218  cmpsub  23263  uncmp  23266  dfconn2  23282  cnconn  23285  1stcfb  23308  txuni2  23428  txbas  23430  ptbasin  23440  txcls  23467  txbasval  23469  txlly  23499  txnlly  23500  pthaus  23501  txlm  23511  tx1stc  23513  xkohaus  23516  isufil2  23771  ufileu  23782  cnpflfi  23862  txflf  23869  fclscf  23888  flimfnfcls  23891  alexsubb  23909  alexsubALTlem2  23911  alexsubALTlem4  23913  ptcmplem2  23916  ptcmplem3  23917  cnextcn  23930  qustgplem  23984  prdsmet  24234  blin2  24293  prdsbl  24355  nmolb  24581  tgqioo  24664  reconnlem2  24692  reconn  24693  lebnumlem3  24838  iscau4  25155  cmetcaulem  25164  iscmet3lem2  25168  bcthlem5  25204  minveclem3b  25304  pmltpc  25327  evthicc2  25337  ovolunlem2  25375  ovolicc2lem5  25398  mblsplit  25409  iundisj2  25426  volsup  25433  ioombl1lem4  25438  dyaddisj  25473  dyadmbllem  25476  i1faddlem  25570  itg10a  25587  itg1ge0a  25588  mbfi1flimlem  25599  mbfmullem  25602  itg2add  25636  rolle  25870  dvcvx  25901  itgsubst  25932  tdeglem4  25941  ply1domn  26005  fta1b  26053  plyadd  26098  plymul  26099  coeeu  26106  vieta1  26196  aalioulem6  26221  ulmcaulem  26279  ulmcau  26280  ulmbdd  26283  ulmcn  26284  amgm  26877  mumullem2  27066  ppiublem1  27089  dchrfi  27142  dchrptlem2  27152  dchrptlem3  27153  dchrsum2  27155  lgsdchr  27242  lgsquad2lem2  27272  2sqlem5  27309  2sqb  27319  pntlemp  27497  ostthlem2  27515  ostth  27526  nosupprefixmo  27588  noinfprefixmo  27589  noetasuplem4  27624  madebdaylemlrcut  27786  addsproplem2  27853  precsexlem11  28095  sltonold  28138  iscgrglt  28417  tgbtwnconn1  28478  colline  28552  lmimid  28697  axcontlem8  28874  axcontlem9  28875  eengtrkg  28889  numedglnl  29047  uhgr2edg  29111  uspgr2wlkeq  29549  wlkonl1iedg  29567  wlkdlem2  29585  pthdlem2  29671  clwlkclwwlklem2a4  29899  clwwisshclwwsn  29918  clwwlknon1sn  30002  frgr2wwlkeu  30229  frgrreg  30296  frgrregord013  30297  nvmul0or  30552  ubthlem3  30774  axhcompl-zf  30900  hvmul0or  30927  ocnel  31200  pjhthmo  31204  spanuni  31446  spansni  31459  hon0  31695  leopadd  32034  leoptr  32039  mdsymlem6  32310  sumdmdlem2  32321  cdjreui  32334  iundisj2f  32492  disjunsn  32496  iundisj2fi  32693  ballotlemimin  34470  bnj23  34681  bnj594  34875  bnj849  34888  cusgr3cyclex  35096  txsconn  35201  cvmsdisj  35230  cvmliftlem15  35258  cvmlift2lem10  35272  cvmlift3lem7  35285  fmla1  35347  satffunlem1lem2  35363  satffunlem2lem2  35366  mclsppslem  35543  dfon2lem3  35746  dfon2lem5  35748  dfon2lem6  35749  dfon2lem7  35750  dfon2lem8  35751  ifscgr  36005  cgr3tr4  36013  btwnconn1lem13  36060  seglecgr12  36072  elicc3  36278  neibastop1  36320  tailfb  36338  bj-sblem2  36804  bj-sngltag  36944  copsex2d  37100  mptsnunlem  37299  finxpreclem6  37357  wl-equsal1i  37505  lindsenlbs  37582  poimirlem26  37613  poimirlem27  37614  ismblfin  37628  itg2addnclem3  37640  ftc1anclem6  37665  fdc  37712  riscer  37955  intidl  37996  ispridlc  38037  disjlem14  38763  disjlem17  38764  prtlem14  38840  prtlem17  38842  lpssat  38979  lssatle  38981  lshpkrlem6  39081  cvrnbtwn  39237  atlatmstc  39285  atlatle  39286  atlrelat1  39287  2at0mat0  39492  trlator0  40138  cdleme0moN  40192  cdlemn11pre  41177  dihord2pre  41192  dihmeetlem20N  41293  dochkrshp4  41356  lcfl6  41467  expeqidd  42286  remullid  42395  diophin  42733  diophun  42734  inaex  44259  pm10.57  44333  modelaxreplem1  44941  fnchoice  44996  ellimcabssub0  45588  fourierdlem81  46158  fourierdlem93  46170  2reuimp0  47088  fzopredsuc  47297  2ffzoeq  47301  m1modmmod  47332  iccpartlt  47398  ichnreuop  47446  prmdvdsfmtnof1lem1  47558  lighneallem4  47584  odd2prm2  47692  even3prm2  47693  sbgoldbst  47752  nnsum4primesevenALTV  47775  stgrvtx0  47934  isubgr3stgrlem6  47943  pgnbgreunbgr  48088  ply1mulgsumlem1  48348  snlindsntor  48433  islininds2  48446  itschlc0xyqsol1  48728  2itscp  48743  opnneir  48868  iscnrm3lem2  48896