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  1072  nic-ax  1703  19.30  1911  19.33b  1915  sbrimvw  2125  necon1bd  2976  rexlimdvvva  3223  spc2d  3561  pssdifn0  4323  ralnralall  4474  disjss3  5108  somo  5608  frminex  5640  sofld  6185  predtrss  6323  ordelord  6382  unizlim  6485  f0rn0  6763  funopfv  6930  mpteqb  7009  fvrnressn  7158  funfvima  7228  fpropnf1  7265  fliftfun  7310  weniso  7352  tfinds  7852  tfindsg  7853  tfindes  7855  tfinds2  7856  findsg  7890  resf1ext2b  7928  frxp  8118  poxp2  8135  soseq  8151  suppssr  8187  rdgsucmptnf  8412  frsucmptn  8422  tz7.49  8428  om00  8556  oewordi  8573  iiner  8783  eroveu  8806  fsetexb  8857  sdomdif  9109  pssnn  9149  sucdom2  9183  php3  9189  unxpdomlem3  9214  fisseneq  9219  ordunifi  9246  isfinite2  9254  fiint  9282  infssuni  9299  ixpfi2  9303  finsschain  9312  ordtypelem10  9485  wofib  9503  wemapsolem  9508  unxpwdom2  9546  inf3lem2  9594  cantnfp1lem3  9645  cantnfp1  9646  setind  9712  frr3g  9724  r1tr  9744  r1ordg  9746  rankelb  9792  rankxplim3  9849  updjudhf  9913  cardlim  9954  infxpenlem  9993  infxpenc2  10002  dfac5lem4  10106  dfac12k  10127  kmlem13  10142  sornom  10256  fin23lem25  10303  fin23lem21  10318  zorn2lem4  10478  iundom2g  10519  fpwwe2lem11  10621  fpwwe2lem12  10622  pwfseqlem4a  10641  eltsk2g  10731  inttsk  10754  tskord  10760  r1tskina  10762  grudomon  10797  arch  12496  zaddcl  12629  uzm1  12891  xrsupsslem  13328  xrinfmsslem  13329  fsequb  14007  fseqsupubi  14010  ssnn0fi  14017  seqf1o  14075  sq01  14257  ccatalpha  14627  swrdnd0  14691  repsdf2  14811  cshw1  14855  wrdl3s3  14995  rexanre  15394  rexuzre  15400  cau3lem  15402  o1co  15633  rlimcn3  15637  o1of2  15660  lo1add  15674  lo1mul  15675  climcau  15718  climbdd  15719  caucvgb  15727  summo  15764  isumltss  15898  mertenslem2  15935  prodmolem2  15985  prodmo  15986  dvdsaddre2b  16360  bitsfzolem  16487  bitsfzo  16488  bezoutlem4  16595  lcmfeq0b  16683  lcmfunsnlem2  16693  divgcdcoprmex  16719  prmind2  16738  2mulprm  16746  isprm5  16761  prmdvdsbc  16780  prm23ge5  16870  pcqmul  16908  pcadd  16944  prmreclem2  16972  prmreclem5  16975  mul4sq  17009  vdwmc2  17034  ramcl  17084  prmgaplem7  17112  prmlem1a  17161  setsstruct2  17229  divsfval  17596  iscatd2  17732  catpropd  17760  wunfunc  17953  cyccom  19269  gaorber  19373  psgneu  19571  lsmsubm  19718  pj1eu  19761  efgredlem  19812  qusabl  19930  cygctb  19957  lt6abl  19960  gsumval3eu  19969  dprdsubg  20091  ablfac1c  20138  pgpfac1  20147  dvdsrtr  20446  unitgrp  20461  abvn0b  20939  lvecvs0or  21232  lspdisjb  21250  lspsolvlem  21266  lspprat  21277  lbsextlem2  21283  nzerooringczr  21630  domnchr  21682  znfld  21710  cygznlem3  21719  obselocv  21878  cpmatacl  22873  chfacfisf  23011  chfacfisfcpmat  23012  0ntr  23228  opnneiid  23283  restntr  23339  hausnei2  23510  nrmsep3  23512  cmpsub  23557  uncmp  23560  dfconn2  23576  cnconn  23579  1stcfb  23602  txuni2  23722  txbas  23724  ptbasin  23734  txcls  23761  txbasval  23763  txlly  23793  txnlly  23794  pthaus  23795  txlm  23805  tx1stc  23807  xkohaus  23810  isufil2  24065  ufileu  24076  cnpflfi  24156  txflf  24163  fclscf  24182  flimfnfcls  24185  alexsubb  24203  alexsubALTlem2  24205  alexsubALTlem4  24207  ptcmplem2  24210  ptcmplem3  24211  cnextcn  24224  qustgplem  24278  prdsmet  24527  blin2  24586  prdsbl  24648  nmolb  24874  tgqioo  24957  reconnlem2  24985  reconn  24986  lebnumlem3  25122  iscau4  25438  cmetcaulem  25447  iscmet3lem2  25451  bcthlem5  25487  minveclem3b  25587  pmltpc  25609  evthicc2  25619  ovolunlem2  25657  ovolicc2lem5  25680  mblsplit  25691  iundisj2  25708  volsup  25715  ioombl1lem4  25720  dyaddisj  25755  dyadmbllem  25758  i1faddlem  25852  itg10a  25869  itg1ge0a  25870  mbfi1flimlem  25881  mbfmullem  25884  itg2add  25918  rolle  26149  dvcvx  26179  itgsubst  26208  tdeglem4  26217  ply1domn  26281  fta1b  26329  plyadd  26374  plymul  26375  coeeu  26382  vieta1  26473  aalioulem6  26500  ulmcaulem  26557  ulmcau  26558  ulmbdd  26561  ulmcn  26562  amgm  27155  mumullem2  27344  ppiublem1  27366  dchrfi  27419  dchrptlem2  27429  dchrptlem3  27430  dchrsum2  27432  lgsdchr  27519  lgsquad2lem2  27549  2sqlem5  27586  2sqb  27596  pntlemp  27774  ostthlem2  27792  ostth  27803  nosupprefixmo  27864  noinfprefixmo  27865  noetasuplem4  27900  madebdaylemlrcut  28092  addsproplem2  28163  precsexlem11  28410  ltonold  28454  bdayfinbndlem1  28660  iscgrglt  28783  tgbtwnconn1  28844  colline  28923  lmimid  29103  axcontlem8  29321  axcontlem9  29322  eengtrkg  29336  numedglnl  29494  uhgr2edg  29558  uspgr2wlkeq  29995  wlkonl1iedg  30013  wlkdlem2  30031  pthdlem2  30117  clwlkclwwlklem2a4  30348  clwwisshclwwsn  30367  clwwlknon1sn  30451  frgr2wwlkeu  30678  frgrreg  30745  frgrregord013  30746  nvmul0or  31002  ubthlem3  31224  axhcompl-zf  31350  hvmul0or  31377  ocnel  31650  pjhthmo  31654  spanuni  31896  spansni  31909  hon0  32145  leopadd  32484  leoptr  32489  mdsymlem6  32760  sumdmdlem2  32771  cdjreui  32784  iundisj2f  32935  disjunsn  32939  iundisj2fi  33142  ballotlemimin  34896  bnj23  35107  bnj594  35300  bnj849  35313  setindregs  35543  karddom  35574  kardsdom  35575  cusgr3cyclex  35628  txsconn  35733  cvmsdisj  35762  cvmliftlem15  35790  cvmlift2lem10  35804  cvmlift3lem7  35817  fmla1  35879  satffunlem1lem2  35895  satffunlem2lem2  35898  mclsppslem  36075  dfon2lem3  36275  dfon2lem5  36277  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  ifscgr  36536  cgr3tr4  36544  btwnconn1lem13  36591  seglecgr12  36603  elicc3  36848  neibastop1  36890  tailfb  36908  bj-sblem2  37498  bj-sngltag  37639  copsex2d  37803  mptsnunlem  38004  finxpreclem6  38062  wl-equsal1i  38219  lindsenlbs  38286  poimirlem26  38317  poimirlem27  38318  ismblfin  38332  itg2addnclem3  38344  ftc1anclem6  38369  fdc  38416  riscer  38659  intidl  38700  ispridlc  38741  disjlem14  39570  disjlem17  39571  prtlem14  39668  prtlem17  39670  lpssat  39807  lssatle  39809  lshpkrlem6  39909  cvrnbtwn  40065  atlatmstc  40113  atlatle  40114  atlrelat1  40115  2at0mat0  40319  trlator0  40965  cdleme0moN  41019  cdlemn11pre  42004  dihord2pre  42019  dihmeetlem20N  42120  dochkrshp4  42183  lcfl6  42294  expeqidd  43106  remullid  43215  diophin  43523  diophun  43524  inaex  45027  pm10.57  45101  modelaxreplem1  45707  fnchoice  45769  ellimcabssub0  46353  fourierdlem81  46921  fourierdlem93  46933  2reuimp0  47871  fzopredsuc  48081  2ffzoeq  48085  m1modmmod  48121  iccpartlt  48193  ichnreuop  48241  prmdvdsfmtnof1lem1  48356  lighneallem4  48382  odd2prm2  48503  even3prm2  48504  sbgoldbst  48563  nnsum4primesevenALTV  48586  stgrvtx0  48747  isubgr3stgrlem6  48756  grlimprclnbgrvtx  48784  pgnbgreunbgr  48910  ply1mulgsumlem1  49186  snlindsntor  49271  islininds2  49284  itschlc0xyqsol1  49566  2itscp  49581  opnneir  49705  iscnrm3lem2  49733