Theorem biimtrrid 242

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3g  295  oplem1  1054  nic-ax  1674  19.30  1883  19.33b  1887  necon1bd  2957  spc2d  3592  pssdifn0  4365  ralnralall  4518  disjss3  5147  somo  5625  frminex  5656  sofld  6186  predtrss  6323  ordelord  6386  unizlim  6487  f0rn0  6776  funopfv  6943  mpteqb  7017  fvrnressn  7161  funfvima  7234  fpropnf1  7269  fliftfun  7312  weniso  7354  tfinds  7853  tfindsg  7854  tfindes  7856  tfinds2  7857  findsg  7894  frxp  8116  poxp2  8133  soseq  8149  suppssr  8185  rdgsucmptnf  8433  frsucmptn  8443  tz7.49  8449  om00  8579  oewordi  8595  iiner  8787  eroveu  8810  fsetexb  8862  undomOLD  9064  sucdom2OLD  9086  sdomdif  9129  pssnn  9172  sucdom2  9210  php3  9216  php3OLD  9228  unxpdomlem3  9256  fisseneq  9261  pssnnOLD  9269  ordunifi  9297  isfinite2  9305  fiint  9328  infssuni  9347  ixpfi2  9354  finsschain  9363  ordtypelem10  9526  wofib  9544  wemapsolem  9549  unxpwdom2  9587  inf3lem2  9628  cantnfp1lem3  9679  cantnfp1  9680  setind  9733  frr3g  9755  r1tr  9775  r1ordg  9777  rankelb  9823  rankxplim3  9880  updjudhf  9930  cardlim  9971  infxpenlem  10012  infxpenc2  10021  dfac5lem4  10125  dfac12k  10146  kmlem13  10161  sornom  10276  fin23lem25  10323  fin23lem21  10338  zorn2lem4  10498  iundom2g  10539  fpwwe2lem11  10640  fpwwe2lem12  10641  pwfseqlem4a  10660  eltsk2g  10750  inttsk  10773  tskord  10779  r1tskina  10781  grudomon  10816  arch  12474  zaddcl  12607  uzm1  12865  xrsupsslem  13291  xrinfmsslem  13292  fsequb  13945  fseqsupubi  13948  ssnn0fi  13955  seqf1o  14014  sq01  14193  ccatalpha  14548  swrdnd0  14612  repsdf2  14733  cshw1  14777  wrdl3s3  14918  rexanre  15298  rexuzre  15304  cau3lem  15306  o1co  15535  rlimcn3  15539  o1of2  15562  lo1add  15576  lo1mul  15577  climcau  15622  climbdd  15623  caucvgb  15631  summo  15668  isumltss  15799  mertenslem2  15836  prodmolem2  15884  prodmo  15885  dvdsaddre2b  16255  bitsfzolem  16380  bitsfzo  16381  bezoutlem4  16489  lcmfeq0b  16572  lcmfunsnlem2  16582  divgcdcoprmex  16608  prmind2  16627  2mulprm  16635  isprm5  16649  prm23ge5  16753  pcqmul  16791  pcadd  16827  prmreclem2  16855  prmreclem5  16858  mul4sq  16892  vdwmc2  16917  ramcl  16967  prmgaplem7  16995  prmlem1a  17045  setsstruct2  17112  divsfval  17498  iscatd2  17630  catpropd  17658  wunfunc  17854  wunfuncOLD  17855  cyccom  19119  gaorber  19214  psgneu  19416  lsmsubm  19563  pj1eu  19606  efgredlem  19657  qusabl  19775  cygctb  19802  lt6abl  19805  gsumval3eu  19814  dprdsubg  19936  ablfac1c  19983  pgpfac1  19992  dvdsrtr  20260  unitgrp  20275  drngmul0or  20530  lvecvs0or  20867  lspdisjb  20885  lspsolvlem  20901  lspprat  20912  lbsextlem2  20918  abvn0b  21121  domnchr  21304  znfld  21336  cygznlem3  21345  obselocv  21503  cpmatacl  22439  chfacfisf  22577  chfacfisfcpmat  22578  0ntr  22796  opnneiid  22851  restntr  22907  hausnei2  23078  nrmsep3  23080  cmpsub  23125  uncmp  23128  dfconn2  23144  cnconn  23147  1stcfb  23170  txuni2  23290  txbas  23292  ptbasin  23302  txcls  23329  txbasval  23331  txlly  23361  txnlly  23362  pthaus  23363  txlm  23373  tx1stc  23375  xkohaus  23378  isufil2  23633  ufileu  23644  cnpflfi  23724  txflf  23731  fclscf  23750  flimfnfcls  23753  alexsubb  23771  alexsubALTlem2  23773  alexsubALTlem4  23775  ptcmplem2  23778  ptcmplem3  23779  cnextcn  23792  qustgplem  23846  prdsmet  24097  blin2  24156  prdsbl  24221  nmolb  24455  tgqioo  24537  reconnlem2  24564  reconn  24565  lebnumlem3  24710  iscau4  25028  cmetcaulem  25037  iscmet3lem2  25041  bcthlem5  25077  minveclem3b  25177  pmltpc  25200  evthicc2  25210  ovolunlem2  25248  ovolicc2lem5  25271  mblsplit  25282  iundisj2  25299  volsup  25306  ioombl1lem4  25311  dyaddisj  25346  dyadmbllem  25349  i1faddlem  25443  itg10a  25461  itg1ge0a  25462  mbfi1flimlem  25473  mbfmullem  25476  itg2add  25510  rolle  25743  dvcvx  25773  itgsubst  25802  tdeglem4  25813  tdeglem4OLD  25814  ply1domn  25877  fta1b  25923  plyadd  25967  plymul  25968  coeeu  25975  vieta1  26062  aalioulem6  26087  ulmcaulem  26143  ulmcau  26144  ulmbdd  26147  ulmcn  26148  amgm  26732  mumullem2  26921  ppiublem1  26942  dchrfi  26995  dchrptlem2  27005  dchrptlem3  27006  dchrsum2  27008  lgsdchr  27095  lgsquad2lem2  27125  2sqlem5  27162  2sqb  27172  pntlemp  27350  ostthlem2  27368  ostth  27379  nosupprefixmo  27440  noinfprefixmo  27441  noetasuplem4  27476  madebdaylemlrcut  27631  addsproplem2  27693  precsexlem11  27903  sltonold  27927  iscgrglt  28033  tgbtwnconn1  28094  colline  28168  lmimid  28313  axcontlem8  28497  axcontlem9  28498  eengtrkg  28512  numedglnl  28672  uhgr2edg  28733  uspgr2wlkeq  29171  wlkonl1iedg  29190  wlkdlem2  29208  pthdlem2  29293  clwlkclwwlklem2a4  29518  clwwisshclwwsn  29537  clwwlknon1sn  29621  frgr2wwlkeu  29848  frgrreg  29915  frgrregord013  29916  nvmul0or  30171  ubthlem3  30393  axhcompl-zf  30519  hvmul0or  30546  ocnel  30819  pjhthmo  30823  spanuni  31065  spansni  31078  hon0  31314  leopadd  31653  leoptr  31658  mdsymlem6  31929  sumdmdlem2  31940  cdjreui  31953  iundisj2f  32089  disjunsn  32093  iundisj2fi  32276  prmdvdsbc  32290  ballotlemimin  33803  bnj23  34028  bnj594  34222  bnj849  34235  cusgr3cyclex  34426  txsconn  34531  cvmsdisj  34560  cvmliftlem15  34588  cvmlift2lem10  34602  cvmlift3lem7  34615  fmla1  34677  satffunlem1lem2  34693  satffunlem2lem2  34696  mclsppslem  34873  dfon2lem3  35062  dfon2lem5  35064  dfon2lem6  35065  dfon2lem7  35066  dfon2lem8  35067  ifscgr  35321  cgr3tr4  35329  btwnconn1lem13  35376  seglecgr12  35388  elicc3  35506  neibastop1  35548  tailfb  35566  bj-sblem2  36026  bj-sngltag  36168  copsex2d  36324  mptsnunlem  36523  finxpreclem6  36581  wl-equsal1i  36716  lindsenlbs  36787  poimirlem26  36818  poimirlem27  36819  ismblfin  36833  itg2addnclem3  36845  ftc1anclem6  36870  fdc  36917  riscer  37160  intidl  37201  ispridlc  37242  disjlem14  37972  disjlem17  37973  prtlem14  38048  prtlem17  38050  lpssat  38187  lssatle  38189  lshpkrlem6  38289  cvrnbtwn  38445  atlatmstc  38493  atlatle  38494  atlrelat1  38495  2at0mat0  38700  trlator0  39346  cdleme0moN  39400  cdlemn11pre  40385  dihord2pre  40400  dihmeetlem20N  40501  dochkrshp4  40564  lcfl6  40675  remullid  41609  diophin  41813  diophun  41814  inaex  43359  pm10.57  43433  fnchoice  44016  ellimcabssub0  44632  fourierdlem81  45202  fourierdlem93  45214  2reuimp0  46121  fzopredsuc  46330  2ffzoeq  46335  iccpartlt  46391  ichnreuop  46439  prmdvdsfmtnof1lem1  46551  lighneallem4  46577  odd2prm2  46685  even3prm2  46686  sbgoldbst  46745  nnsum4primesevenALTV  46768  nzerooringczr  47059  ply1mulgsumlem1  47155  snlindsntor  47240  islininds2  47253  m1modmmod  47295  itschlc0xyqsol1  47540  2itscp  47555  opnneir  47627  iscnrm3lem2  47655