Theorem syl5bir 232

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 217	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bir.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 33	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  3imtr3g  283  oplem1  999  nic-ax  1589  19.30  1798  19.33b  1802  hbntOLD  2130  necon1bd  2800  pssdifn0  3898  ssdisjOLD  3979  disjss3  4582  somo  4993  frminex  5018  sofld  5500  ordelord  5662  unizlim  5761  f0rn0  6003  funopfv  6145  mpteqb  6207  fvrnressn  6333  funfvima  6396  fliftfun  6462  weniso  6504  tfinds  6951  tfindsg  6952  tfindes  6954  tfinds2  6955  findsg  6985  frxp  7174  suppssr  7213  rdgsucmptnf  7412  frsucmptn  7421  tz7.49  7427  om00  7542  oewordi  7558  iiner  7706  eroveu  7729  undom  7933  sdomdif  7993  php3  8031  sucdom2  8041  unxpdomlem3  8051  fisseneq  8056  pssnn  8063  ordunifi  8095  isfinite2  8103  fiint  8122  infssuni  8140  ixpfi2  8147  finsschain  8156  ordtypelem10  8315  wofib  8333  wemapsolem  8338  unxpwdom2  8376  inf3lem2  8409  cantnfp1lem3  8460  cantnfp1  8461  setind  8493  r1tr  8522  r1ordg  8524  rankelb  8570  rankxplim3  8627  cardlim  8681  infxpenlem  8719  infxpenc2  8728  dfac5lem4  8832  dfac12k  8852  kmlem13  8867  sornom  8982  fin23lem25  9029  fin23lem21  9044  zorn2lem4  9204  iundom2g  9241  fpwwe2lem12  9342  fpwwe2lem13  9343  pwfseqlem4a  9362  eltsk2g  9452  inttsk  9475  tskord  9481  r1tskina  9483  grudomon  9518  arch  11166  zaddcl  11294  uzm1  11594  xrsupsslem  12009  xrinfmsslem  12010  fsequb  12636  fseqsupubi  12639  ssnn0fi  12646  seqf1o  12704  sq01  12848  ccatalpha  13228  swrdccatin1  13334  repsdf2  13376  cshw1  13419  wrdl3s3  13553  rexanre  13934  rexuzre  13940  cau3lem  13942  o1co  14165  rlimcn2  14169  o1of2  14191  lo1add  14205  lo1mul  14206  climcau  14249  climbdd  14250  caucvgb  14258  summo  14295  isumltss  14419  mertenslem2  14456  prodmolem2  14504  prodmo  14505  dvdsaddre2b  14867  bitsfzolem  14994  bitsfzo  14995  bezoutlem4  15097  lcmfeq0b  15181  lcmfunsnlem2  15191  divgcdcoprmex  15218  prmind2  15236  isprm5  15257  prm23ge5  15358  pcqmul  15396  pcadd  15431  prmreclem2  15459  prmreclem5  15462  mul4sq  15496  vdwmc2  15521  ramcl  15571  prmgaplem7  15599  prmlem1a  15651  divsfval  16030  iscatd2  16165  catpropd  16192  wunfunc  16382  gaorber  17564  psgneu  17749  lsmsubm  17891  pj1eu  17932  efgredlem  17983  qusabl  18091  cygabl  18115  cygctb  18116  lt6abl  18119  gsumval3eu  18128  dprdsubg  18246  ablfac1c  18293  pgpfac1  18302  dvdsrtr  18475  unitgrp  18490  drngmul0or  18591  lvecvs0or  18929  lspdisjb  18947  lspsolvlem  18963  lspprat  18974  lbsextlem2  18980  abvn0b  19123  domnchr  19699  znfld  19728  cygznlem3  19737  obselocv  19891  cpmatacl  20340  chfacfisf  20478  chfacfisfcpmat  20479  0ntr  20685  opnneiid  20740  restntr  20796  hausnei2  20967  nrmsep3  20969  cmpsub  21013  uncmp  21016  dfcon2  21032  cnconn  21035  1stcfb  21058  txuni2  21178  txbas  21180  ptbasin  21190  txcls  21217  txbasval  21219  txlly  21249  txnlly  21250  pthaus  21251  txlm  21261  tx1stc  21263  xkohaus  21266  isufil2  21522  ufileu  21533  cnpflfi  21613  txflf  21620  fclscf  21639  flimfnfcls  21642  alexsubb  21660  alexsubALTlem2  21662  alexsubALTlem4  21664  ptcmplem2  21667  ptcmplem3  21668  cnextcn  21681  qustgplem  21734  prdsmet  21985  blin2  22044  prdsbl  22106  nmolb  22331  tgqioo  22411  reconnlem2  22438  reconn  22439  lebnumlem3  22570  iscau4  22885  cmetcaulem  22894  iscmet3lem2  22898  bcthlem5  22933  minveclem3b  23007  pmltpc  23026  evthicc2  23036  ovolunlem2  23073  ovolicc2lem5  23096  mblsplit  23107  iundisj2  23124  volsup  23131  ioombl1lem4  23136  dyaddisj  23170  dyadmbllem  23173  i1faddlem  23266  itg10a  23283  itg1ge0a  23284  mbfi1flimlem  23295  mbfmullem  23298  itg2add  23332  rolle  23557  dvcvx  23587  itgsubst  23616  tdeglem4  23624  ply1domn  23687  fta1b  23733  plyadd  23777  plymul  23778  coeeu  23785  vieta1  23871  aalioulem6  23896  ulmcaulem  23952  ulmcau  23953  ulmbdd  23956  ulmcn  23957  amgm  24517  mumullem2  24706  ppiublem1  24727  dchrfi  24780  dchrptlem2  24790  dchrptlem3  24791  dchrsum2  24793  lgsdchr  24880  lgsquad2lem2  24910  2sqlem5  24947  2sqb  24957  pntlemp  25099  ostthlem2  25117  ostth  25128  iscgrglt  25209  tgbtwnconn1  25270  colline  25344  lmimid  25486  axcontlem8  25651  axcontlem9  25652  eengtrkg  25665  structgrssvtxlem  25700  usgra2edg  25911  usg2wlkeq  26236  clwlkisclwwlklem2a4  26312  clwwisshclwwn  26336  frgraregord013  26645  nvmul0or  26889  ubthlem3  27112  axhcompl-zf  27239  hvmul0or  27266  ocnel  27541  pjhthmo  27545  spanuni  27787  spansni  27800  hon0  28036  leopadd  28375  leoptr  28380  mdsymlem6  28651  sumdmdlem2  28662  cdjreui  28675  spc2d  28697  iundisj2f  28785  disjunsn  28789  iundisj2fi  28943  ballotlemimin  29894  bnj23  30038  bnj594  30236  bnj849  30249  txscon  30477  cvmsdisj  30506  cvmliftlem15  30534  cvmlift2lem10  30548  cvmlift3lem7  30561  mclsppslem  30734  dfon2lem3  30934  dfon2lem5  30936  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  soseq  30995  frr3g  31023  nodenselem4  31083  nodenselem5  31084  nobndup  31099  nobnddown  31100  ifscgr  31321  cgr3tr4  31329  btwnconn1lem13  31376  seglecgr12  31388  elicc3  31481  neibastop1  31524  tailfb  31542  bj-sngltag  32164  bj-elid  32262  mptsnunlem  32361  finxpreclem6  32409  wl-equsal1i  32508  lindsenlbs  32574  poimirlem26  32605  poimirlem27  32606  ismblfin  32620  itg2addnclem3  32633  ftc1anclem6  32660  fdc  32711  riscer  32957  intidl  32998  ispridlc  33039  prtlem14  33177  prtlem17  33179  lpssat  33318  lssatle  33320  lshpkrlem6  33420  cvrnbtwn  33576  atlatmstc  33624  atlatle  33625  atlrelat1  33626  2at0mat0  33829  trlator0  34476  cdleme0moN  34530  cdlemn11pre  35517  dihord2pre  35532  dihmeetlem20N  35633  dochkrshp4  35696  lcfl6  35807  diophin  36354  diophun  36355  pm10.57  37592  fnchoice  38211  ellimcabssub0  38684  fourierdlem81  39080  fourierdlem93  39092  fzopredsuc  39946  iccpartlt  39962  prmdvdsfmtnof1lem1  40034  lighneallem4  40065  bgoldbst  40200  nnsum4primesevenALTV  40217  cshword2  40300  ralnralall  40307  fpropnf1  40337  2ffzoeq  40361  uhgr2edg  40435  uspgr2wlkeq  40854  wlkOnl1iedg  40873  1wlkdlem2  40892  pthdlem2  40974  clwlkclwwlklem2a4  41206  clwwisshclwwsn  41236  av-frgrareg  41548  av-frgraregord013  41549  nzerooringczr  41864  ply1mulgsumlem1  41968  snlindsntor  42054  islininds2  42067  m1modmmod  42110