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  1673  19.30  1881  19.33b  1885  necon1bd  2958  rexlimdvvva  3214  spc2d  3602  pssdifn0  4368  ralnralall  4515  disjss3  5142  somo  5631  frminex  5664  sofld  6207  predtrss  6343  ordelord  6406  unizlim  6507  f0rn0  6793  funopfv  6958  mpteqb  7035  fvrnressn  7181  funfvima  7250  fpropnf1  7287  fliftfun  7332  weniso  7374  tfinds  7881  tfindsg  7882  tfindes  7884  tfinds2  7885  findsg  7919  resf1ext2b  7957  frxp  8151  poxp2  8168  soseq  8184  suppssr  8220  rdgsucmptnf  8469  frsucmptn  8479  tz7.49  8485  om00  8613  oewordi  8629  iiner  8829  eroveu  8852  fsetexb  8904  undomOLD  9100  sucdom2OLD  9122  sdomdif  9165  pssnn  9208  sucdom2  9243  php3  9249  php3OLD  9261  unxpdomlem3  9288  fisseneq  9293  ordunifi  9326  isfinite2  9334  fiint  9366  fiintOLD  9367  infssuni  9386  ixpfi2  9390  finsschain  9399  ordtypelem10  9567  wofib  9585  wemapsolem  9590  unxpwdom2  9628  inf3lem2  9669  cantnfp1lem3  9720  cantnfp1  9721  setind  9774  frr3g  9796  r1tr  9816  r1ordg  9818  rankelb  9864  rankxplim3  9921  updjudhf  9971  cardlim  10012  infxpenlem  10053  infxpenc2  10062  dfac5lem4  10166  dfac5lem4OLD  10168  dfac12k  10188  kmlem13  10203  sornom  10317  fin23lem25  10364  fin23lem21  10379  zorn2lem4  10539  iundom2g  10580  fpwwe2lem11  10681  fpwwe2lem12  10682  pwfseqlem4a  10701  eltsk2g  10791  inttsk  10814  tskord  10820  r1tskina  10822  grudomon  10857  arch  12523  zaddcl  12657  uzm1  12916  xrsupsslem  13349  xrinfmsslem  13350  fsequb  14016  fseqsupubi  14019  ssnn0fi  14026  seqf1o  14084  sq01  14264  ccatalpha  14631  swrdnd0  14695  repsdf2  14816  cshw1  14860  wrdl3s3  15001  rexanre  15385  rexuzre  15391  cau3lem  15393  o1co  15622  rlimcn3  15626  o1of2  15649  lo1add  15663  lo1mul  15664  climcau  15707  climbdd  15708  caucvgb  15716  summo  15753  isumltss  15884  mertenslem2  15921  prodmolem2  15971  prodmo  15972  dvdsaddre2b  16344  bitsfzolem  16471  bitsfzo  16472  bezoutlem4  16579  lcmfeq0b  16667  lcmfunsnlem2  16677  divgcdcoprmex  16703  prmind2  16722  2mulprm  16730  isprm5  16744  prmdvdsbc  16763  prm23ge5  16853  pcqmul  16891  pcadd  16927  prmreclem2  16955  prmreclem5  16958  mul4sq  16992  vdwmc2  17017  ramcl  17067  prmgaplem7  17095  prmlem1a  17144  setsstruct2  17211  divsfval  17592  iscatd2  17724  catpropd  17752  wunfunc  17946  cyccom  19221  gaorber  19326  psgneu  19524  lsmsubm  19671  pj1eu  19714  efgredlem  19765  qusabl  19883  cygctb  19910  lt6abl  19913  gsumval3eu  19922  dprdsubg  20044  ablfac1c  20091  pgpfac1  20100  dvdsrtr  20368  unitgrp  20383  drngmul0orOLD  20761  abvn0b  20837  lvecvs0or  21110  lspdisjb  21128  lspsolvlem  21144  lspprat  21155  lbsextlem2  21161  nzerooringczr  21491  domnchr  21547  znfld  21579  cygznlem3  21588  obselocv  21748  cpmatacl  22722  chfacfisf  22860  chfacfisfcpmat  22861  0ntr  23079  opnneiid  23134  restntr  23190  hausnei2  23361  nrmsep3  23363  cmpsub  23408  uncmp  23411  dfconn2  23427  cnconn  23430  1stcfb  23453  txuni2  23573  txbas  23575  ptbasin  23585  txcls  23612  txbasval  23614  txlly  23644  txnlly  23645  pthaus  23646  txlm  23656  tx1stc  23658  xkohaus  23661  isufil2  23916  ufileu  23927  cnpflfi  24007  txflf  24014  fclscf  24033  flimfnfcls  24036  alexsubb  24054  alexsubALTlem2  24056  alexsubALTlem4  24058  ptcmplem2  24061  ptcmplem3  24062  cnextcn  24075  qustgplem  24129  prdsmet  24380  blin2  24439  prdsbl  24504  nmolb  24738  tgqioo  24821  reconnlem2  24849  reconn  24850  lebnumlem3  24995  iscau4  25313  cmetcaulem  25322  iscmet3lem2  25326  bcthlem5  25362  minveclem3b  25462  pmltpc  25485  evthicc2  25495  ovolunlem2  25533  ovolicc2lem5  25556  mblsplit  25567  iundisj2  25584  volsup  25591  ioombl1lem4  25596  dyaddisj  25631  dyadmbllem  25634  i1faddlem  25728  itg10a  25745  itg1ge0a  25746  mbfi1flimlem  25757  mbfmullem  25760  itg2add  25794  rolle  26028  dvcvx  26059  itgsubst  26090  tdeglem4  26099  ply1domn  26163  fta1b  26211  plyadd  26256  plymul  26257  coeeu  26264  vieta1  26354  aalioulem6  26379  ulmcaulem  26437  ulmcau  26438  ulmbdd  26441  ulmcn  26442  amgm  27034  mumullem2  27223  ppiublem1  27246  dchrfi  27299  dchrptlem2  27309  dchrptlem3  27310  dchrsum2  27312  lgsdchr  27399  lgsquad2lem2  27429  2sqlem5  27466  2sqb  27476  pntlemp  27654  ostthlem2  27672  ostth  27683  nosupprefixmo  27745  noinfprefixmo  27746  noetasuplem4  27781  madebdaylemlrcut  27937  addsproplem2  28003  precsexlem11  28241  sltonold  28283  iscgrglt  28522  tgbtwnconn1  28583  colline  28657  lmimid  28802  axcontlem8  28986  axcontlem9  28987  eengtrkg  29001  numedglnl  29161  uhgr2edg  29225  uspgr2wlkeq  29664  wlkonl1iedg  29683  wlkdlem2  29701  pthdlem2  29788  clwlkclwwlklem2a4  30016  clwwisshclwwsn  30035  clwwlknon1sn  30119  frgr2wwlkeu  30346  frgrreg  30413  frgrregord013  30414  nvmul0or  30669  ubthlem3  30891  axhcompl-zf  31017  hvmul0or  31044  ocnel  31317  pjhthmo  31321  spanuni  31563  spansni  31576  hon0  31812  leopadd  32151  leoptr  32156  mdsymlem6  32427  sumdmdlem2  32438  cdjreui  32451  iundisj2f  32603  disjunsn  32607  iundisj2fi  32799  ballotlemimin  34508  bnj23  34732  bnj594  34926  bnj849  34939  cusgr3cyclex  35141  txsconn  35246  cvmsdisj  35275  cvmliftlem15  35303  cvmlift2lem10  35317  cvmlift3lem7  35330  fmla1  35392  satffunlem1lem2  35408  satffunlem2lem2  35411  mclsppslem  35588  dfon2lem3  35786  dfon2lem5  35788  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  ifscgr  36045  cgr3tr4  36053  btwnconn1lem13  36100  seglecgr12  36112  elicc3  36318  neibastop1  36360  tailfb  36378  bj-sblem2  36844  bj-sngltag  36984  copsex2d  37140  mptsnunlem  37339  finxpreclem6  37397  wl-equsal1i  37545  lindsenlbs  37622  poimirlem26  37653  poimirlem27  37654  ismblfin  37668  itg2addnclem3  37680  ftc1anclem6  37705  fdc  37752  riscer  37995  intidl  38036  ispridlc  38077  disjlem14  38799  disjlem17  38800  prtlem14  38875  prtlem17  38877  lpssat  39014  lssatle  39016  lshpkrlem6  39116  cvrnbtwn  39272  atlatmstc  39320  atlatle  39321  atlrelat1  39322  2at0mat0  39527  trlator0  40173  cdleme0moN  40227  cdlemn11pre  41212  dihord2pre  41227  dihmeetlem20N  41328  dochkrshp4  41391  lcfl6  41502  expeqidd  42360  remullid  42463  diophin  42783  diophun  42784  inaex  44316  pm10.57  44390  modelaxreplem1  44995  fnchoice  45034  ellimcabssub0  45632  fourierdlem81  46202  fourierdlem93  46214  2reuimp0  47126  fzopredsuc  47335  2ffzoeq  47339  iccpartlt  47411  ichnreuop  47459  prmdvdsfmtnof1lem1  47571  lighneallem4  47597  odd2prm2  47705  even3prm2  47706  sbgoldbst  47765  nnsum4primesevenALTV  47788  stgrvtx0  47929  isubgr3stgrlem6  47938  ply1mulgsumlem1  48303  snlindsntor  48388  islininds2  48401  m1modmmod  48442  itschlc0xyqsol1  48687  2itscp  48702  opnneir  48804  iscnrm3lem2  48832