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  1057  nic-ax  1675  19.30  1883  19.33b  1887  necon1bd  2951  rexlimdvvva  3196  spc2d  3558  pssdifn0  4322  ralnralall  4468  disjss3  5099  somo  5579  frminex  5611  sofld  6153  predtrss  6288  ordelord  6347  unizlim  6449  f0rn0  6727  funopfv  6891  mpteqb  6969  fvrnressn  7116  funfvima  7186  fpropnf1  7223  fliftfun  7268  weniso  7310  tfinds  7812  tfindsg  7813  tfindes  7815  tfinds2  7816  findsg  7849  resf1ext2b  7887  frxp  8078  poxp2  8095  soseq  8111  suppssr  8147  rdgsucmptnf  8370  frsucmptn  8380  tz7.49  8386  om00  8512  oewordi  8529  iiner  8738  eroveu  8761  fsetexb  8813  sdomdif  9065  pssnn  9105  sucdom2  9139  php3  9145  unxpdomlem3  9170  fisseneq  9175  ordunifi  9202  isfinite2  9210  fiint  9239  infssuni  9258  ixpfi2  9262  finsschain  9271  ordtypelem10  9444  wofib  9462  wemapsolem  9467  unxpwdom2  9505  inf3lem2  9550  cantnfp1lem3  9601  cantnfp1  9602  setind  9668  frr3g  9680  r1tr  9700  r1ordg  9702  rankelb  9748  rankxplim3  9805  updjudhf  9855  cardlim  9896  infxpenlem  9935  infxpenc2  9944  dfac5lem4  10048  dfac5lem4OLD  10050  dfac12k  10070  kmlem13  10085  sornom  10199  fin23lem25  10246  fin23lem21  10261  zorn2lem4  10421  iundom2g  10462  fpwwe2lem11  10564  fpwwe2lem12  10565  pwfseqlem4a  10584  eltsk2g  10674  inttsk  10697  tskord  10703  r1tskina  10705  grudomon  10740  arch  12410  zaddcl  12543  uzm1  12797  xrsupsslem  13234  xrinfmsslem  13235  fsequb  13910  fseqsupubi  13913  ssnn0fi  13920  seqf1o  13978  sq01  14160  ccatalpha  14529  swrdnd0  14593  repsdf2  14713  cshw1  14757  wrdl3s3  14897  rexanre  15282  rexuzre  15288  cau3lem  15290  o1co  15521  rlimcn3  15525  o1of2  15548  lo1add  15562  lo1mul  15563  climcau  15606  climbdd  15607  caucvgb  15615  summo  15652  isumltss  15783  mertenslem2  15820  prodmolem2  15870  prodmo  15871  dvdsaddre2b  16246  bitsfzolem  16373  bitsfzo  16374  bezoutlem4  16481  lcmfeq0b  16569  lcmfunsnlem2  16579  divgcdcoprmex  16605  prmind2  16624  2mulprm  16632  isprm5  16646  prmdvdsbc  16665  prm23ge5  16755  pcqmul  16793  pcadd  16829  prmreclem2  16857  prmreclem5  16860  mul4sq  16894  vdwmc2  16919  ramcl  16969  prmgaplem7  16997  prmlem1a  17046  setsstruct2  17113  divsfval  17480  iscatd2  17616  catpropd  17644  wunfunc  17837  cyccom  19144  gaorber  19249  psgneu  19447  lsmsubm  19594  pj1eu  19637  efgredlem  19688  qusabl  19806  cygctb  19833  lt6abl  19836  gsumval3eu  19845  dprdsubg  19967  ablfac1c  20014  pgpfac1  20023  dvdsrtr  20316  unitgrp  20331  drngmul0orOLD  20706  abvn0b  20781  lvecvs0or  21075  lspdisjb  21093  lspsolvlem  21109  lspprat  21120  lbsextlem2  21126  nzerooringczr  21447  domnchr  21499  znfld  21527  cygznlem3  21536  obselocv  21695  cpmatacl  22672  chfacfisf  22810  chfacfisfcpmat  22811  0ntr  23027  opnneiid  23082  restntr  23138  hausnei2  23309  nrmsep3  23311  cmpsub  23356  uncmp  23359  dfconn2  23375  cnconn  23378  1stcfb  23401  txuni2  23521  txbas  23523  ptbasin  23533  txcls  23560  txbasval  23562  txlly  23592  txnlly  23593  pthaus  23594  txlm  23604  tx1stc  23606  xkohaus  23609  isufil2  23864  ufileu  23875  cnpflfi  23955  txflf  23962  fclscf  23981  flimfnfcls  23984  alexsubb  24002  alexsubALTlem2  24004  alexsubALTlem4  24006  ptcmplem2  24009  ptcmplem3  24010  cnextcn  24023  qustgplem  24077  prdsmet  24326  blin2  24385  prdsbl  24447  nmolb  24673  tgqioo  24756  reconnlem2  24784  reconn  24785  lebnumlem3  24930  iscau4  25247  cmetcaulem  25256  iscmet3lem2  25260  bcthlem5  25296  minveclem3b  25396  pmltpc  25419  evthicc2  25429  ovolunlem2  25467  ovolicc2lem5  25490  mblsplit  25501  iundisj2  25518  volsup  25525  ioombl1lem4  25530  dyaddisj  25565  dyadmbllem  25568  i1faddlem  25662  itg10a  25679  itg1ge0a  25680  mbfi1flimlem  25691  mbfmullem  25694  itg2add  25728  rolle  25962  dvcvx  25993  itgsubst  26024  tdeglem4  26033  ply1domn  26097  fta1b  26145  plyadd  26190  plymul  26191  coeeu  26198  vieta1  26288  aalioulem6  26313  ulmcaulem  26371  ulmcau  26372  ulmbdd  26375  ulmcn  26376  amgm  26969  mumullem2  27158  ppiublem1  27181  dchrfi  27234  dchrptlem2  27244  dchrptlem3  27245  dchrsum2  27247  lgsdchr  27334  lgsquad2lem2  27364  2sqlem5  27401  2sqb  27411  pntlemp  27589  ostthlem2  27607  ostth  27618  nosupprefixmo  27680  noinfprefixmo  27681  noetasuplem4  27716  madebdaylemlrcut  27907  addsproplem2  27978  precsexlem11  28225  ltonold  28269  bdayfinbndlem1  28475  iscgrglt  28598  tgbtwnconn1  28659  colline  28733  lmimid  28878  axcontlem8  29056  axcontlem9  29057  eengtrkg  29071  numedglnl  29229  uhgr2edg  29293  uspgr2wlkeq  29731  wlkonl1iedg  29749  wlkdlem2  29767  pthdlem2  29853  clwlkclwwlklem2a4  30084  clwwisshclwwsn  30103  clwwlknon1sn  30187  frgr2wwlkeu  30414  frgrreg  30481  frgrregord013  30482  nvmul0or  30738  ubthlem3  30960  axhcompl-zf  31086  hvmul0or  31113  ocnel  31386  pjhthmo  31390  spanuni  31632  spansni  31645  hon0  31881  leopadd  32220  leoptr  32225  mdsymlem6  32496  sumdmdlem2  32507  cdjreui  32520  iundisj2f  32677  disjunsn  32681  iundisj2fi  32888  ballotlemimin  34684  bnj23  34895  bnj594  35088  bnj849  35101  setindregs  35308  cusgr3cyclex  35352  txsconn  35457  cvmsdisj  35486  cvmliftlem15  35514  cvmlift2lem10  35528  cvmlift3lem7  35541  fmla1  35603  satffunlem1lem2  35619  satffunlem2lem2  35622  mclsppslem  35799  dfon2lem3  35999  dfon2lem5  36001  dfon2lem6  36002  dfon2lem7  36003  dfon2lem8  36004  ifscgr  36260  cgr3tr4  36268  btwnconn1lem13  36315  seglecgr12  36327  elicc3  36533  neibastop1  36575  tailfb  36593  bj-sblem2  37091  bj-sngltag  37231  copsex2d  37394  mptsnunlem  37593  finxpreclem6  37651  wl-equsal1i  37799  lindsenlbs  37866  poimirlem26  37897  poimirlem27  37898  ismblfin  37912  itg2addnclem3  37924  ftc1anclem6  37949  fdc  37996  riscer  38239  intidl  38280  ispridlc  38321  disjlem14  39152  disjlem17  39153  prtlem14  39250  prtlem17  39252  lpssat  39389  lssatle  39391  lshpkrlem6  39491  cvrnbtwn  39647  atlatmstc  39695  atlatle  39696  atlrelat1  39697  2at0mat0  39901  trlator0  40547  cdleme0moN  40601  cdlemn11pre  41586  dihord2pre  41601  dihmeetlem20N  41702  dochkrshp4  41765  lcfl6  41876  expeqidd  42695  remullid  42804  diophin  43129  diophun  43130  inaex  44653  pm10.57  44727  modelaxreplem1  45334  fnchoice  45389  ellimcabssub0  45977  fourierdlem81  46545  fourierdlem93  46557  2reuimp0  47474  fzopredsuc  47683  2ffzoeq  47687  m1modmmod  47718  iccpartlt  47784  ichnreuop  47832  prmdvdsfmtnof1lem1  47944  lighneallem4  47970  odd2prm2  48078  even3prm2  48079  sbgoldbst  48138  nnsum4primesevenALTV  48161  stgrvtx0  48322  isubgr3stgrlem6  48331  grlimprclnbgrvtx  48359  pgnbgreunbgr  48485  ply1mulgsumlem1  48746  snlindsntor  48831  islininds2  48844  itschlc0xyqsol1  49126  2itscp  49141  opnneir  49266  iscnrm3lem2  49294