Theorem syl5bir 245

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
syl5bir.1	⊢ (𝜓 ↔ 𝜑)
syl5bir.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5bir	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5bir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 230	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bir.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3g  297  oplem1  1051  nic-ax  1674  19.30  1882  19.33b  1886  necon1bd  3034  spc2d  3603  pssdifn0  4325  ralnralall  4458  disjss3  5065  somo  5510  frminex  5535  sofld  6044  ordelord  6213  unizlim  6307  f0rn0  6564  funopfv  6717  mpteqb  6787  fvrnressn  6923  funfvima  6992  fpropnf1  7025  fliftfun  7065  weniso  7107  tfinds  7574  tfindsg  7575  tfindes  7577  tfinds2  7578  findsg  7609  frxp  7820  suppssr  7861  rdgsucmptnf  8065  frsucmptn  8074  tz7.49  8081  om00  8201  oewordi  8217  iiner  8369  eroveu  8392  undom  8605  sdomdif  8665  php3  8703  sucdom2  8714  unxpdomlem3  8724  fisseneq  8729  pssnn  8736  ordunifi  8768  isfinite2  8776  fiint  8795  infssuni  8815  ixpfi2  8822  finsschain  8831  ordtypelem10  8991  wofib  9009  wemapsolem  9014  unxpwdom2  9052  inf3lem2  9092  cantnfp1lem3  9143  cantnfp1  9144  setind  9176  r1tr  9205  r1ordg  9207  rankelb  9253  rankxplim3  9310  updjudhf  9360  cardlim  9401  infxpenlem  9439  infxpenc2  9448  dfac5lem4  9552  dfac12k  9573  kmlem13  9588  sornom  9699  fin23lem25  9746  fin23lem21  9761  zorn2lem4  9921  iundom2g  9962  fpwwe2lem12  10063  fpwwe2lem13  10064  pwfseqlem4a  10083  eltsk2g  10173  inttsk  10196  tskord  10202  r1tskina  10204  grudomon  10239  arch  11895  zaddcl  12023  uzm1  12277  xrsupsslem  12701  xrinfmsslem  12702  fsequb  13344  fseqsupubi  13347  ssnn0fi  13354  seqf1o  13412  sq01  13587  ccatalpha  13947  swrdnd0  14019  repsdf2  14140  cshw1  14184  wrdl3s3  14326  rexanre  14706  rexuzre  14712  cau3lem  14714  o1co  14943  rlimcn2  14947  o1of2  14969  lo1add  14983  lo1mul  14984  climcau  15027  climbdd  15028  caucvgb  15036  summo  15074  isumltss  15203  mertenslem2  15241  prodmolem2  15289  prodmo  15290  dvdsaddre2b  15657  bitsfzolem  15783  bitsfzo  15784  bezoutlem4  15890  lcmfeq0b  15974  lcmfunsnlem2  15984  divgcdcoprmex  16010  prmind2  16029  2mulprm  16037  isprm5  16051  prm23ge5  16152  pcqmul  16190  pcadd  16225  prmreclem2  16253  prmreclem5  16256  mul4sq  16290  vdwmc2  16315  ramcl  16365  prmgaplem7  16393  prmlem1a  16440  setsstruct2  16521  divsfval  16820  iscatd2  16952  catpropd  16979  wunfunc  17169  cyccom  18346  gaorber  18438  psgneu  18634  lsmsubm  18778  pj1eu  18822  efgredlem  18873  qusabl  18985  cygablOLD  19011  cygctb  19012  lt6abl  19015  gsumval3eu  19024  dprdsubg  19146  ablfac1c  19193  pgpfac1  19202  dvdsrtr  19402  unitgrp  19417  drngmul0or  19523  lvecvs0or  19880  lspdisjb  19898  lspsolvlem  19914  lspprat  19925  lbsextlem2  19931  abvn0b  20075  domnchr  20679  znfld  20707  cygznlem3  20716  obselocv  20872  cpmatacl  21324  chfacfisf  21462  chfacfisfcpmat  21463  0ntr  21679  opnneiid  21734  restntr  21790  hausnei2  21961  nrmsep3  21963  cmpsub  22008  uncmp  22011  dfconn2  22027  cnconn  22030  1stcfb  22053  txuni2  22173  txbas  22175  ptbasin  22185  txcls  22212  txbasval  22214  txlly  22244  txnlly  22245  pthaus  22246  txlm  22256  tx1stc  22258  xkohaus  22261  isufil2  22516  ufileu  22527  cnpflfi  22607  txflf  22614  fclscf  22633  flimfnfcls  22636  alexsubb  22654  alexsubALTlem2  22656  alexsubALTlem4  22658  ptcmplem2  22661  ptcmplem3  22662  cnextcn  22675  qustgplem  22729  prdsmet  22980  blin2  23039  prdsbl  23101  nmolb  23326  tgqioo  23408  reconnlem2  23435  reconn  23436  lebnumlem3  23567  iscau4  23882  cmetcaulem  23891  iscmet3lem2  23895  bcthlem5  23931  minveclem3b  24031  pmltpc  24051  evthicc2  24061  ovolunlem2  24099  ovolicc2lem5  24122  mblsplit  24133  iundisj2  24150  volsup  24157  ioombl1lem4  24162  dyaddisj  24197  dyadmbllem  24200  i1faddlem  24294  itg10a  24311  itg1ge0a  24312  mbfi1flimlem  24323  mbfmullem  24326  itg2add  24360  rolle  24587  dvcvx  24617  itgsubst  24646  tdeglem4  24654  ply1domn  24717  fta1b  24763  plyadd  24807  plymul  24808  coeeu  24815  vieta1  24901  aalioulem6  24926  ulmcaulem  24982  ulmcau  24983  ulmbdd  24986  ulmcn  24987  amgm  25568  mumullem2  25757  ppiublem1  25778  dchrfi  25831  dchrptlem2  25841  dchrptlem3  25842  dchrsum2  25844  lgsdchr  25931  lgsquad2lem2  25961  2sqlem5  25998  2sqb  26008  pntlemp  26186  ostthlem2  26204  ostth  26215  iscgrglt  26300  tgbtwnconn1  26361  colline  26435  lmimid  26580  axcontlem8  26757  axcontlem9  26758  eengtrkg  26772  numedglnl  26929  uhgr2edg  26990  uspgr2wlkeq  27427  wlkonl1iedg  27447  wlkdlem2  27465  pthdlem2  27549  clwlkclwwlklem2a4  27775  clwwisshclwwsn  27794  clwwlknon1sn  27879  frgr2wwlkeu  28106  frgrreg  28173  frgrregord013  28174  nvmul0or  28427  ubthlem3  28649  axhcompl-zf  28775  hvmul0or  28802  ocnel  29075  pjhthmo  29079  spanuni  29321  spansni  29334  hon0  29570  leopadd  29909  leoptr  29914  mdsymlem6  30185  sumdmdlem2  30196  cdjreui  30209  iundisj2f  30340  disjunsn  30344  iundisj2fi  30520  prmdvdsbc  30532  ballotlemimin  31763  bnj23  31988  bnj594  32184  bnj849  32197  cusgr3cyclex  32383  txsconn  32488  cvmsdisj  32517  cvmliftlem15  32545  cvmlift2lem10  32559  cvmlift3lem7  32572  fmla1  32634  satffunlem1lem2  32650  satffunlem2lem2  32653  mclsppslem  32830  dfon2lem3  33030  dfon2lem5  33032  dfon2lem6  33033  dfon2lem7  33034  dfon2lem8  33035  soseq  33096  frr3g  33121  noprefixmo  33202  noetalem3  33219  ifscgr  33505  cgr3tr4  33513  btwnconn1lem13  33560  seglecgr12  33572  elicc3  33665  neibastop1  33707  tailfb  33725  bj-sblem2  34167  bj-sngltag  34298  copsex2d  34434  mptsnunlem  34622  finxpreclem6  34680  wl-equsal1i  34798  lindsenlbs  34902  poimirlem26  34933  poimirlem27  34934  ismblfin  34948  itg2addnclem3  34960  ftc1anclem6  34987  fdc  35035  riscer  35281  intidl  35322  ispridlc  35363  prtlem14  36025  prtlem17  36027  lpssat  36164  lssatle  36166  lshpkrlem6  36266  cvrnbtwn  36422  atlatmstc  36470  atlatle  36471  atlrelat1  36472  2at0mat0  36676  trlator0  37322  cdleme0moN  37376  cdlemn11pre  38361  dihord2pre  38376  dihmeetlem20N  38477  dochkrshp4  38540  lcfl6  38651  remulid2  39298  diophin  39418  diophun  39419  inaex  40682  pm10.57  40752  fnchoice  41335  ellimcabssub0  41947  fourierdlem81  42521  fourierdlem93  42533  2reuimp0  43362  fzopredsuc  43572  2ffzoeq  43577  iccpartlt  43633  ichnreuop  43683  prmdvdsfmtnof1lem1  43795  lighneallem4  43824  odd2prm2  43932  even3prm2  43933  sbgoldbst  43992  nnsum4primesevenALTV  44015  nzerooringczr  44392  ply1mulgsumlem1  44489  snlindsntor  44575  islininds2  44588  m1modmmod  44630  itschlc0xyqsol1  44802  2itscp  44817