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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3g  298  oplem1  1072  nic-ax  1706  19.30  1916  19.33b  1920  sbrimvw  2130  necon1bd  2977  rexlimdvvva  3224  spc2d  3560  pssdifn0  4319  ralnralall  4472  disjss3  5107  somo  5605  frminex  5637  sofld  6197  predtrss  6351  ordelord  6410  unizlim  6513  f0rn0  6797  funopfv  6965  mpteqb  7044  fvrnressn  7197  funfvima  7267  fpropnf1  7302  fliftfun  7351  weniso  7395  tfinds  7905  tfindsg  7906  tfindes  7908  tfinds2  7909  findsg  7943  resf1ext2b  7981  frxp  8175  poxp2  8197  soseq  8213  suppssr  8250  rdgsucmptnf  8475  frsucmptn  8485  tz7.49  8493  om00  8621  oewordi  8638  iiner  8848  eroveu  8871  fsetexb  8924  sdomdif  9182  pssnn  9222  sucdom2  9256  php3  9262  unxpdomlem3  9287  fisseneq  9292  ordunifi  9319  isfinite2  9328  fiint  9356  infssuni  9373  ixpfi2  9377  finsschain  9386  ordtypelem10  9558  wofib  9576  wemapsolem  9581  unxpwdom2  9619  inf3lem2  9667  cantnfp1lem3  9718  cantnfp1  9719  setind  9785  frr3g  9797  r1tr  9820  r1ordg  9822  rankelb  9870  rankxplim3  9935  updjudhf  10049  cardlim  10090  infxpenlem  10131  infxpenc2  10140  dfac5lem4  10244  dfac12k  10265  kmlem13  10280  sornom  10394  fin23lem25  10441  fin23lem21  10456  zorn2lem4  10616  iundom2g  10663  fpwwe2lem11  10765  fpwwe2lem12  10766  pwfseqlem4a  10785  eltsk2g  10875  inttsk  10898  tskord  10904  r1tskina  10906  grudomon  10941  arch  12643  zaddcl  12776  uzm1  13039  xrsupsslem  13477  xrinfmsslem  13478  fsequb  14158  fseqsupubi  14161  ssnn0fi  14168  seqf1o  14226  sq01  14410  ccatalpha  14781  swrdnd0  14849  repsdf2  14971  cshw1  15015  wrdl3s3  15158  rexanre  15558  rexuzre  15564  cau3lem  15566  o1co  15797  rlimcn3  15801  o1of2  15824  lo1add  15838  lo1mul  15839  climcau  15882  climbdd  15883  caucvgb  15891  summo  15927  isumltss  16061  mertenslem2  16098  prodmolem2  16146  prodmo  16147  dvdsaddre2b  16521  bitsfzolem  16648  bitsfzo  16649  bezoutlem4  16759  lcmfeq0b  16849  lcmfunsnlem2  16859  divgcdcoprmex  16885  prmind2  16904  2mulprm  16912  isprm5  16927  prmdvdsbc  16946  prm23ge5  17037  pcqmul  17075  pcadd  17111  prmreclem2  17139  prmreclem5  17142  mul4sq  17176  vdwmc2  17201  ramcl  17251  prmgaplem7  17279  prmlem1a  17328  setsstruct2  17396  divsfval  17769  iscatd2  17905  catpropd  17933  wunfunc  18126  cyccom  19468  gaorber  19573  psgneu  19771  lsmsubm  19918  pj1eu  19961  efgredlem  20012  qusabl  20130  cygctb  20157  lt6abl  20160  gsumval3eu  20169  dprdsubg  20291  ablfac1c  20338  pgpfac1  20347  dvdsrtr  20649  unitgrp  20664  abvn0b  21144  lvecvs0or  21437  lspdisjb  21455  lspsolvlem  21471  lspprat  21482  lbsextlem2  21488  nzerooringczr  21841  domnchr  21893  znfld  21921  cygznlem3  21930  obselocv  22089  lindsenlbs  22212  cpmatacl  23089  chfacfisf  23227  chfacfisfcpmat  23228  0ntr  23444  opnneiid  23499  restntr  23555  hausnei2  23726  nrmsep3  23728  cmpsub  23773  uncmp  23776  dfconn2  23792  cnconn  23795  1stcfb  23818  txuni2  23939  txbas  23941  ptbasin  23951  txcls  23978  txbasval  23980  txlly  24010  txnlly  24011  pthaus  24012  txlm  24022  tx1stc  24024  xkohaus  24027  isufil2  24282  ufileu  24293  cnpflfi  24373  txflf  24380  fclscf  24399  flimfnfcls  24402  alexsubb  24420  alexsubALTlem2  24422  alexsubALTlem4  24424  ptcmplem2  24427  ptcmplem3  24428  cnextcn  24441  qustgplem  24495  prdsmet  24744  blin2  24803  prdsbl  24865  nmolb  25091  tgqioo  25174  reconnlem2  25202  reconn  25203  lebnumlem3  25339  iscau4  25655  cmetcaulem  25664  iscmet3lem2  25668  bcthlem5  25704  minveclem3b  25804  pmltpc  25826  evthicc2  25836  ovolunlem2  25874  ovolicc2lem5  25897  mblsplit  25908  iundisj2  25925  volsup  25932  ioombl1lem4  25937  dyaddisj  25972  dyadmbllem  25975  i1faddlem  26069  itg10a  26086  itg1ge0a  26087  mbfi1flimlem  26098  mbfmullem  26101  itg2add  26135  rolle  26365  dvcvx  26395  itgsubst  26424  tdeglem4  26433  ply1domn  26497  fta1b  26545  plyadd  26591  plymul  26592  coeeu  26599  vieta1  26690  aalioulem6  26721  ulmcaulem  26778  ulmcau  26779  ulmbdd  26782  ulmcn  26783  amgm  27375  mumullem2  27564  ppiublem1  27586  dchrfi  27639  dchrptlem2  27649  dchrptlem3  27650  dchrsum2  27652  lgsdchr  27739  lgsquad2lem2  27769  2sqlem5  27806  2sqb  27816  pntlemp  27994  ostthlem2  28012  ostth  28023  nosupprefixmo  28114  noinfprefixmo  28115  noetasuplem4  28150  madebdaylemlrcut  28342  addsproplem2  28413  precsexlem11  28660  ltonold  28704  bdayfinbndlem1  28910  iscgrglt  29034  tgbtwnconn1  29095  colline  29175  lmimid  29356  axcontlem8  29606  axcontlem9  29607  eengtrkg  29621  numedglnl  29779  uhgr2edg  29846  uspgr2wlkeq  30283  wlkonl1iedg  30301  wlkdlem2  30319  pthdlem2  30411  clwlkclwwlklem2a4  30645  clwwisshclwwsn  30664  clwwlknon1sn  30748  frgr2wwlkeu  30985  frgrreg  31052  frgrregord013  31053  nvmul0or  31309  ubthlem3  31531  axhcompl-zf  31657  hvmul0or  31684  ocnel  31957  pjhthmo  31961  spanuni  32203  spansni  32216  hon0  32452  leopadd  32791  leoptr  32796  mdsymlem6  33067  sumdmdlem2  33078  cdjreui  33091  iundisj2f  33282  disjunsn  33286  iundisj2fi  33485  zzedom  33958  ballotlemimin  35249  bnj23  35460  bnj594  35653  bnj849  35666  setindregs  35939  karddom  35970  kardsdom  35971  j00smo  36046  cusgr3cyclex  36109  txsconn  36214  cvmsdisj  36243  cvmliftlem15  36271  cvmlift2lem10  36285  cvmlift3lem7  36298  fmla1  36360  satffunlem1lem2  36376  satffunlem2lem2  36379  mclsppslem  36556  dfon2lem3  36762  dfon2lem5  36764  dfon2lem6  36765  dfon2lem7  36766  dfon2lem8  36767  ifscgr  37024  cgr3tr4  37032  btwnconn1lem13  37079  seglecgr12  37091  elicc3  37320  neibastop1  37362  tailfb  37380  bj-sblem2  37970  bj-sngltag  38111  copsex2d  38331  mptsnunlem  38529  finxpreclem6  38587  wl-equsal1i  38744  poimirlem26  38832  poimirlem27  38833  ismblfin  38847  itg2addnclem3  38859  ftc1anclem6  38884  fdc  38945  riscer  39188  intidl  39229  ispridlc  39270  disjlem14  40099  disjlem17  40100  prtlem14  40197  prtlem17  40199  lpssat  40336  lssatle  40338  lshpkrlem6  40438  cvrnbtwn  40594  atlatmstc  40642  atlatle  40643  atlrelat1  40644  2at0mat0  40848  trlator0  41494  cdleme0moN  41548  cdlemn11pre  42533  dihord2pre  42548  dihmeetlem20N  42649  dochkrshp4  42712  lcfl6  42823  expeqidd  43648  remullid  43751  diophin  44049  diophun  44050  inaex  45542  pm10.57  45616  modelaxreplem1  46232  fnchoice  46320  ellimcabssub0  46902  fourierdlem81  47470  fourierdlem93  47482  2reuimp0  48458  fzopredsuc  48667  2ffzoeq  48671  m1modmmod  48707  iccpartlt  48779  ichnreuop  48827  prmdvdsfmtnof1lem1  48942  lighneallem4  48968  odd2prm2  49089  even3prm2  49090  sbgoldbst  49149  nnsum4primesevenALTV  49172  stgrvtx0  49333  isubgr3stgrlem6  49342  grlimprclnbgrvtx  49370  pgnbgreunbgr  49496  ply1mulgsumlem1  49829  snlindsntor  49914  islininds2  49927  itschlc0xyqsol1  50209  2itscp  50224  opnneir  50352  iscnrm3lem2  50380