Theorem biimtrrid 246

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3g  298  oplem1  1070  nic-ax  1700  19.30  1908  19.33b  1912  sbrimvw  2131  necon1bd  2982  rexlimdvvva  3229  spc2d  3570  pssdifn0  4331  ralnralall  4479  disjss3  5112  somo  5609  frminex  5641  sofld  6186  predtrss  6324  ordelord  6383  unizlim  6486  f0rn0  6764  funopfv  6931  mpteqb  7010  fvrnressn  7159  funfvima  7229  fpropnf1  7266  fliftfun  7311  weniso  7353  tfinds  7855  tfindsg  7856  tfindes  7858  tfinds2  7859  findsg  7893  resf1ext2b  7931  frxp  8121  poxp2  8138  soseq  8154  suppssr  8190  rdgsucmptnf  8415  frsucmptn  8425  tz7.49  8431  om00  8559  oewordi  8576  iiner  8786  eroveu  8809  fsetexb  8860  sdomdif  9112  pssnn  9152  sucdom2  9186  php3  9192  unxpdomlem3  9217  fisseneq  9222  ordunifi  9249  isfinite2  9257  fiint  9285  infssuni  9302  ixpfi2  9306  finsschain  9315  ordtypelem10  9488  wofib  9506  wemapsolem  9511  unxpwdom2  9549  inf3lem2  9597  cantnfp1lem3  9648  cantnfp1  9649  setind  9715  frr3g  9727  r1tr  9747  r1ordg  9749  rankelb  9795  rankxplim3  9852  updjudhf  9916  cardlim  9957  infxpenlem  9996  infxpenc2  10005  dfac5lem4  10109  dfac12k  10130  kmlem13  10145  sornom  10260  fin23lem25  10307  fin23lem21  10322  zorn2lem4  10482  iundom2g  10523  fpwwe2lem11  10625  fpwwe2lem12  10626  pwfseqlem4a  10645  eltsk2g  10735  inttsk  10758  tskord  10764  r1tskina  10766  grudomon  10801  arch  12500  zaddcl  12633  uzm1  12895  xrsupsslem  13332  xrinfmsslem  13333  fsequb  14010  fseqsupubi  14013  ssnn0fi  14020  seqf1o  14078  sq01  14260  ccatalpha  14630  swrdnd0  14694  repsdf2  14814  cshw1  14858  wrdl3s3  14998  rexanre  15397  rexuzre  15403  cau3lem  15405  o1co  15636  rlimcn3  15640  o1of2  15663  lo1add  15677  lo1mul  15678  climcau  15721  climbdd  15722  caucvgb  15730  summo  15767  isumltss  15901  mertenslem2  15938  prodmolem2  15988  prodmo  15989  dvdsaddre2b  16364  bitsfzolem  16491  bitsfzo  16492  bezoutlem4  16599  lcmfeq0b  16687  lcmfunsnlem2  16697  divgcdcoprmex  16723  prmind2  16742  2mulprm  16750  isprm5  16765  prmdvdsbc  16784  prm23ge5  16874  pcqmul  16912  pcadd  16948  prmreclem2  16976  prmreclem5  16979  mul4sq  17013  vdwmc2  17038  ramcl  17088  prmgaplem7  17116  prmlem1a  17165  setsstruct2  17233  divsfval  17600  iscatd2  17736  catpropd  17764  wunfunc  17957  cyccom  19273  gaorber  19377  psgneu  19575  lsmsubm  19722  pj1eu  19765  efgredlem  19816  qusabl  19934  cygctb  19961  lt6abl  19964  gsumval3eu  19973  dprdsubg  20095  ablfac1c  20142  pgpfac1  20151  dvdsrtr  20449  unitgrp  20464  abvn0b  20916  lvecvs0or  21209  lspdisjb  21227  lspsolvlem  21243  lspprat  21254  lbsextlem2  21260  nzerooringczr  21598  domnchr  21650  znfld  21678  cygznlem3  21687  obselocv  21846  cpmatacl  22841  chfacfisf  22979  chfacfisfcpmat  22980  0ntr  23196  opnneiid  23251  restntr  23307  hausnei2  23478  nrmsep3  23480  cmpsub  23525  uncmp  23528  dfconn2  23544  cnconn  23547  1stcfb  23570  txuni2  23690  txbas  23692  ptbasin  23702  txcls  23729  txbasval  23731  txlly  23761  txnlly  23762  pthaus  23763  txlm  23773  tx1stc  23775  xkohaus  23778  isufil2  24033  ufileu  24044  cnpflfi  24124  txflf  24131  fclscf  24150  flimfnfcls  24153  alexsubb  24171  alexsubALTlem2  24173  alexsubALTlem4  24175  ptcmplem2  24178  ptcmplem3  24179  cnextcn  24192  qustgplem  24246  prdsmet  24495  blin2  24554  prdsbl  24616  nmolb  24842  tgqioo  24925  reconnlem2  24953  reconn  24954  lebnumlem3  25090  iscau4  25406  cmetcaulem  25415  iscmet3lem2  25419  bcthlem5  25455  minveclem3b  25555  pmltpc  25577  evthicc2  25587  ovolunlem2  25625  ovolicc2lem5  25648  mblsplit  25659  iundisj2  25676  volsup  25683  ioombl1lem4  25688  dyaddisj  25723  dyadmbllem  25726  i1faddlem  25820  itg10a  25837  itg1ge0a  25838  mbfi1flimlem  25849  mbfmullem  25852  itg2add  25886  rolle  26117  dvcvx  26147  itgsubst  26176  tdeglem4  26185  ply1domn  26249  fta1b  26297  plyadd  26342  plymul  26343  coeeu  26350  vieta1  26441  aalioulem6  26466  ulmcaulem  26522  ulmcau  26523  ulmbdd  26526  ulmcn  26527  amgm  27120  mumullem2  27309  ppiublem1  27331  dchrfi  27384  dchrptlem2  27394  dchrptlem3  27395  dchrsum2  27397  lgsdchr  27484  lgsquad2lem2  27514  2sqlem5  27551  2sqb  27561  pntlemp  27739  ostthlem2  27757  ostth  27768  nosupprefixmo  27829  noinfprefixmo  27830  noetasuplem4  27865  madebdaylemlrcut  28057  addsproplem2  28128  precsexlem11  28375  ltonold  28419  bdayfinbndlem1  28625  iscgrglt  28748  tgbtwnconn1  28809  colline  28884  lmimid  29060  axcontlem8  29261  axcontlem9  29262  eengtrkg  29276  numedglnl  29434  uhgr2edg  29498  uspgr2wlkeq  29935  wlkonl1iedg  29953  wlkdlem2  29971  pthdlem2  30057  clwlkclwwlklem2a4  30288  clwwisshclwwsn  30307  clwwlknon1sn  30391  frgr2wwlkeu  30618  frgrreg  30685  frgrregord013  30686  nvmul0or  30942  ubthlem3  31164  axhcompl-zf  31290  hvmul0or  31317  ocnel  31590  pjhthmo  31594  spanuni  31836  spansni  31849  hon0  32085  leopadd  32424  leoptr  32429  mdsymlem6  32700  sumdmdlem2  32711  cdjreui  32724  iundisj2f  32875  disjunsn  32879  iundisj2fi  33082  ballotlemimin  34840  bnj23  35051  bnj594  35244  bnj849  35257  setindregs  35465  cusgr3cyclex  35526  txsconn  35631  cvmsdisj  35660  cvmliftlem15  35688  cvmlift2lem10  35702  cvmlift3lem7  35715  fmla1  35777  satffunlem1lem2  35793  satffunlem2lem2  35796  mclsppslem  35973  dfon2lem3  36173  dfon2lem5  36175  dfon2lem6  36176  dfon2lem7  36177  dfon2lem8  36178  ifscgr  36434  cgr3tr4  36442  btwnconn1lem13  36489  seglecgr12  36501  elicc3  36716  neibastop1  36758  tailfb  36776  bj-sblem2  37366  bj-sngltag  37506  copsex2d  37670  mptsnunlem  37871  finxpreclem6  37929  wl-equsal1i  38086  lindsenlbs  38153  poimirlem26  38184  poimirlem27  38185  ismblfin  38199  itg2addnclem3  38211  ftc1anclem6  38236  fdc  38283  riscer  38526  intidl  38567  ispridlc  38608  disjlem14  39439  disjlem17  39440  prtlem14  39537  prtlem17  39539  lpssat  39676  lssatle  39678  lshpkrlem6  39778  cvrnbtwn  39934  atlatmstc  39982  atlatle  39983  atlrelat1  39984  2at0mat0  40188  trlator0  40834  cdleme0moN  40888  cdlemn11pre  41873  dihord2pre  41888  dihmeetlem20N  41989  dochkrshp4  42052  lcfl6  42163  expeqidd  42975  remullid  43084  diophin  43394  diophun  43395  inaex  44898  pm10.57  44972  modelaxreplem1  45578  fnchoice  45640  ellimcabssub0  46224  fourierdlem81  46792  fourierdlem93  46804  2reuimp0  47739  fzopredsuc  47949  2ffzoeq  47953  m1modmmod  47989  iccpartlt  48061  ichnreuop  48109  prmdvdsfmtnof1lem1  48224  lighneallem4  48250  odd2prm2  48371  even3prm2  48372  sbgoldbst  48431  nnsum4primesevenALTV  48454  stgrvtx0  48615  isubgr3stgrlem6  48624  grlimprclnbgrvtx  48652  pgnbgreunbgr  48778  ply1mulgsumlem1  49050  snlindsntor  49135  islininds2  49148  itschlc0xyqsol1  49430  2itscp  49445  opnneir  49569  iscnrm3lem2  49597