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  1674  19.30  1882  19.33b  1886  necon1bd  2946  rexlimdvvva  3190  spc2d  3552  pssdifn0  4313  ralnralall  4460  disjss3  5085  somo  5558  frminex  5590  sofld  6129  predtrss  6264  ordelord  6323  unizlim  6425  f0rn0  6703  funopfv  6866  mpteqb  6943  fvrnressn  7089  funfvima  7159  fpropnf1  7196  fliftfun  7241  weniso  7283  tfinds  7785  tfindsg  7786  tfindes  7788  tfinds2  7789  findsg  7822  resf1ext2b  7860  frxp  8051  poxp2  8068  soseq  8084  suppssr  8120  rdgsucmptnf  8343  frsucmptn  8353  tz7.49  8359  om00  8485  oewordi  8501  iiner  8708  eroveu  8731  fsetexb  8783  sdomdif  9033  pssnn  9073  sucdom2  9107  php3  9113  unxpdomlem3  9137  fisseneq  9142  ordunifi  9169  isfinite2  9177  fiint  9206  infssuni  9225  ixpfi2  9229  finsschain  9238  ordtypelem10  9408  wofib  9426  wemapsolem  9431  unxpwdom2  9469  inf3lem2  9514  cantnfp1lem3  9565  cantnfp1  9566  setind  9632  frr3g  9644  r1tr  9664  r1ordg  9666  rankelb  9712  rankxplim3  9769  updjudhf  9819  cardlim  9860  infxpenlem  9899  infxpenc2  9908  dfac5lem4  10012  dfac5lem4OLD  10014  dfac12k  10034  kmlem13  10049  sornom  10163  fin23lem25  10210  fin23lem21  10225  zorn2lem4  10385  iundom2g  10426  fpwwe2lem11  10527  fpwwe2lem12  10528  pwfseqlem4a  10547  eltsk2g  10637  inttsk  10660  tskord  10666  r1tskina  10668  grudomon  10703  arch  12373  zaddcl  12507  uzm1  12765  xrsupsslem  13201  xrinfmsslem  13202  fsequb  13877  fseqsupubi  13880  ssnn0fi  13887  seqf1o  13945  sq01  14127  ccatalpha  14496  swrdnd0  14560  repsdf2  14680  cshw1  14724  wrdl3s3  14864  rexanre  15249  rexuzre  15255  cau3lem  15257  o1co  15488  rlimcn3  15492  o1of2  15515  lo1add  15529  lo1mul  15530  climcau  15573  climbdd  15574  caucvgb  15582  summo  15619  isumltss  15750  mertenslem2  15787  prodmolem2  15837  prodmo  15838  dvdsaddre2b  16213  bitsfzolem  16340  bitsfzo  16341  bezoutlem4  16448  lcmfeq0b  16536  lcmfunsnlem2  16546  divgcdcoprmex  16572  prmind2  16591  2mulprm  16599  isprm5  16613  prmdvdsbc  16632  prm23ge5  16722  pcqmul  16760  pcadd  16796  prmreclem2  16824  prmreclem5  16827  mul4sq  16861  vdwmc2  16886  ramcl  16936  prmgaplem7  16964  prmlem1a  17013  setsstruct2  17080  divsfval  17446  iscatd2  17582  catpropd  17610  wunfunc  17803  cyccom  19110  gaorber  19215  psgneu  19413  lsmsubm  19560  pj1eu  19603  efgredlem  19654  qusabl  19772  cygctb  19799  lt6abl  19802  gsumval3eu  19811  dprdsubg  19933  ablfac1c  19980  pgpfac1  19989  dvdsrtr  20281  unitgrp  20296  drngmul0orOLD  20671  abvn0b  20746  lvecvs0or  21040  lspdisjb  21058  lspsolvlem  21074  lspprat  21085  lbsextlem2  21091  nzerooringczr  21412  domnchr  21464  znfld  21492  cygznlem3  21501  obselocv  21660  cpmatacl  22626  chfacfisf  22764  chfacfisfcpmat  22765  0ntr  22981  opnneiid  23036  restntr  23092  hausnei2  23263  nrmsep3  23265  cmpsub  23310  uncmp  23313  dfconn2  23329  cnconn  23332  1stcfb  23355  txuni2  23475  txbas  23477  ptbasin  23487  txcls  23514  txbasval  23516  txlly  23546  txnlly  23547  pthaus  23548  txlm  23558  tx1stc  23560  xkohaus  23563  isufil2  23818  ufileu  23829  cnpflfi  23909  txflf  23916  fclscf  23935  flimfnfcls  23938  alexsubb  23956  alexsubALTlem2  23958  alexsubALTlem4  23960  ptcmplem2  23963  ptcmplem3  23964  cnextcn  23977  qustgplem  24031  prdsmet  24280  blin2  24339  prdsbl  24401  nmolb  24627  tgqioo  24710  reconnlem2  24738  reconn  24739  lebnumlem3  24884  iscau4  25201  cmetcaulem  25210  iscmet3lem2  25214  bcthlem5  25250  minveclem3b  25350  pmltpc  25373  evthicc2  25383  ovolunlem2  25421  ovolicc2lem5  25444  mblsplit  25455  iundisj2  25472  volsup  25479  ioombl1lem4  25484  dyaddisj  25519  dyadmbllem  25522  i1faddlem  25616  itg10a  25633  itg1ge0a  25634  mbfi1flimlem  25645  mbfmullem  25648  itg2add  25682  rolle  25916  dvcvx  25947  itgsubst  25978  tdeglem4  25987  ply1domn  26051  fta1b  26099  plyadd  26144  plymul  26145  coeeu  26152  vieta1  26242  aalioulem6  26267  ulmcaulem  26325  ulmcau  26326  ulmbdd  26329  ulmcn  26330  amgm  26923  mumullem2  27112  ppiublem1  27135  dchrfi  27188  dchrptlem2  27198  dchrptlem3  27199  dchrsum2  27201  lgsdchr  27288  lgsquad2lem2  27318  2sqlem5  27355  2sqb  27365  pntlemp  27543  ostthlem2  27561  ostth  27572  nosupprefixmo  27634  noinfprefixmo  27635  noetasuplem4  27670  madebdaylemlrcut  27839  addsproplem2  27908  precsexlem11  28150  sltonold  28193  iscgrglt  28487  tgbtwnconn1  28548  colline  28622  lmimid  28767  axcontlem8  28944  axcontlem9  28945  eengtrkg  28959  numedglnl  29117  uhgr2edg  29181  uspgr2wlkeq  29619  wlkonl1iedg  29637  wlkdlem2  29655  pthdlem2  29741  clwlkclwwlklem2a4  29969  clwwisshclwwsn  29988  clwwlknon1sn  30072  frgr2wwlkeu  30299  frgrreg  30366  frgrregord013  30367  nvmul0or  30622  ubthlem3  30844  axhcompl-zf  30970  hvmul0or  30997  ocnel  31270  pjhthmo  31274  spanuni  31516  spansni  31529  hon0  31765  leopadd  32104  leoptr  32109  mdsymlem6  32380  sumdmdlem2  32391  cdjreui  32404  iundisj2f  32562  disjunsn  32566  iundisj2fi  32771  ballotlemimin  34511  bnj23  34722  bnj594  34916  bnj849  34929  setindregs  35120  cusgr3cyclex  35172  txsconn  35277  cvmsdisj  35306  cvmliftlem15  35334  cvmlift2lem10  35348  cvmlift3lem7  35361  fmla1  35423  satffunlem1lem2  35439  satffunlem2lem2  35442  mclsppslem  35619  dfon2lem3  35819  dfon2lem5  35821  dfon2lem6  35822  dfon2lem7  35823  dfon2lem8  35824  ifscgr  36078  cgr3tr4  36086  btwnconn1lem13  36133  seglecgr12  36145  elicc3  36351  neibastop1  36393  tailfb  36411  bj-sblem2  36877  bj-sngltag  37017  copsex2d  37173  mptsnunlem  37372  finxpreclem6  37430  wl-equsal1i  37578  lindsenlbs  37655  poimirlem26  37686  poimirlem27  37687  ismblfin  37701  itg2addnclem3  37713  ftc1anclem6  37738  fdc  37785  riscer  38028  intidl  38069  ispridlc  38110  disjlem14  38836  disjlem17  38837  prtlem14  38913  prtlem17  38915  lpssat  39052  lssatle  39054  lshpkrlem6  39154  cvrnbtwn  39310  atlatmstc  39358  atlatle  39359  atlrelat1  39360  2at0mat0  39564  trlator0  40210  cdleme0moN  40264  cdlemn11pre  41249  dihord2pre  41264  dihmeetlem20N  41365  dochkrshp4  41428  lcfl6  41539  expeqidd  42358  remullid  42467  diophin  42805  diophun  42806  inaex  44330  pm10.57  44404  modelaxreplem1  45011  fnchoice  45066  ellimcabssub0  45657  fourierdlem81  46225  fourierdlem93  46237  2reuimp0  47145  fzopredsuc  47354  2ffzoeq  47358  m1modmmod  47389  iccpartlt  47455  ichnreuop  47503  prmdvdsfmtnof1lem1  47615  lighneallem4  47641  odd2prm2  47749  even3prm2  47750  sbgoldbst  47809  nnsum4primesevenALTV  47832  stgrvtx0  47993  isubgr3stgrlem6  48002  grlimprclnbgrvtx  48030  pgnbgreunbgr  48156  ply1mulgsumlem1  48418  snlindsntor  48503  islininds2  48516  itschlc0xyqsol1  48798  2itscp  48813  opnneir  48938  iscnrm3lem2  48966