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  1670  19.30  1878  19.33b  1882  necon1bd  3034  spc2d  3603  pssdifn0  4325  ralnralall  4458  disjss3  5058  somo  5505  frminex  5530  sofld  6039  ordelord  6208  unizlim  6302  f0rn0  6559  funopfv  6712  mpteqb  6782  fvrnressn  6918  funfvima  6986  fpropnf1  7019  fliftfun  7059  weniso  7101  tfinds  7568  tfindsg  7569  tfindes  7571  tfinds2  7572  findsg  7603  frxp  7814  suppssr  7855  rdgsucmptnf  8059  frsucmptn  8068  tz7.49  8075  om00  8195  oewordi  8211  iiner  8363  eroveu  8386  undom  8599  sdomdif  8659  php3  8697  sucdom2  8708  unxpdomlem3  8718  fisseneq  8723  pssnn  8730  ordunifi  8762  isfinite2  8770  fiint  8789  infssuni  8809  ixpfi2  8816  finsschain  8825  ordtypelem10  8985  wofib  9003  wemapsolem  9008  unxpwdom2  9046  inf3lem2  9086  cantnfp1lem3  9137  cantnfp1  9138  setind  9170  r1tr  9199  r1ordg  9201  rankelb  9247  rankxplim3  9304  updjudhf  9354  cardlim  9395  infxpenlem  9433  infxpenc2  9442  dfac5lem4  9546  dfac12k  9567  kmlem13  9582  sornom  9693  fin23lem25  9740  fin23lem21  9755  zorn2lem4  9915  iundom2g  9956  fpwwe2lem12  10057  fpwwe2lem13  10058  pwfseqlem4a  10077  eltsk2g  10167  inttsk  10190  tskord  10196  r1tskina  10198  grudomon  10233  arch  11888  zaddcl  12016  uzm1  12270  xrsupsslem  12694  xrinfmsslem  12695  fsequb  13337  fseqsupubi  13340  ssnn0fi  13347  seqf1o  13405  sq01  13580  ccatalpha  13941  swrdnd0  14013  repsdf2  14134  cshw1  14178  wrdl3s3  14320  rexanre  14700  rexuzre  14706  cau3lem  14708  o1co  14937  rlimcn2  14941  o1of2  14963  lo1add  14977  lo1mul  14978  climcau  15021  climbdd  15022  caucvgb  15030  summo  15068  isumltss  15197  mertenslem2  15235  prodmolem2  15283  prodmo  15284  dvdsaddre2b  15651  bitsfzolem  15777  bitsfzo  15778  bezoutlem4  15884  lcmfeq0b  15968  lcmfunsnlem2  15978  divgcdcoprmex  16004  prmind2  16023  2mulprm  16031  isprm5  16045  prm23ge5  16146  pcqmul  16184  pcadd  16219  prmreclem2  16247  prmreclem5  16250  mul4sq  16284  vdwmc2  16309  ramcl  16359  prmgaplem7  16387  prmlem1a  16434  setsstruct2  16515  divsfval  16814  iscatd2  16946  catpropd  16973  wunfunc  17163  cyccom  18340  gaorber  18432  psgneu  18628  lsmsubm  18772  pj1eu  18816  efgredlem  18867  qusabl  18979  cygablOLD  19005  cygctb  19006  lt6abl  19009  gsumval3eu  19018  dprdsubg  19140  ablfac1c  19187  pgpfac1  19196  dvdsrtr  19396  unitgrp  19411  drngmul0or  19517  lvecvs0or  19874  lspdisjb  19892  lspsolvlem  19908  lspprat  19919  lbsextlem2  19925  abvn0b  20069  domnchr  20673  znfld  20701  cygznlem3  20710  obselocv  20866  cpmatacl  21318  chfacfisf  21456  chfacfisfcpmat  21457  0ntr  21673  opnneiid  21728  restntr  21784  hausnei2  21955  nrmsep3  21957  cmpsub  22002  uncmp  22005  dfconn2  22021  cnconn  22024  1stcfb  22047  txuni2  22167  txbas  22169  ptbasin  22179  txcls  22206  txbasval  22208  txlly  22238  txnlly  22239  pthaus  22240  txlm  22250  tx1stc  22252  xkohaus  22255  isufil2  22510  ufileu  22521  cnpflfi  22601  txflf  22608  fclscf  22627  flimfnfcls  22630  alexsubb  22648  alexsubALTlem2  22650  alexsubALTlem4  22652  ptcmplem2  22655  ptcmplem3  22656  cnextcn  22669  qustgplem  22723  prdsmet  22974  blin2  23033  prdsbl  23095  nmolb  23320  tgqioo  23402  reconnlem2  23429  reconn  23430  lebnumlem3  23561  iscau4  23876  cmetcaulem  23885  iscmet3lem2  23889  bcthlem5  23925  minveclem3b  24025  pmltpc  24045  evthicc2  24055  ovolunlem2  24093  ovolicc2lem5  24116  mblsplit  24127  iundisj2  24144  volsup  24151  ioombl1lem4  24156  dyaddisj  24191  dyadmbllem  24194  i1faddlem  24288  itg10a  24305  itg1ge0a  24306  mbfi1flimlem  24317  mbfmullem  24320  itg2add  24354  rolle  24581  dvcvx  24611  itgsubst  24640  tdeglem4  24648  ply1domn  24711  fta1b  24757  plyadd  24801  plymul  24802  coeeu  24809  vieta1  24895  aalioulem6  24920  ulmcaulem  24976  ulmcau  24977  ulmbdd  24980  ulmcn  24981  amgm  25562  mumullem2  25751  ppiublem1  25772  dchrfi  25825  dchrptlem2  25835  dchrptlem3  25836  dchrsum2  25838  lgsdchr  25925  lgsquad2lem2  25955  2sqlem5  25992  2sqb  26002  pntlemp  26180  ostthlem2  26198  ostth  26209  iscgrglt  26294  tgbtwnconn1  26355  colline  26429  lmimid  26574  axcontlem8  26751  axcontlem9  26752  eengtrkg  26766  numedglnl  26923  uhgr2edg  26984  uspgr2wlkeq  27421  wlkonl1iedg  27441  wlkdlem2  27459  pthdlem2  27543  clwlkclwwlklem2a4  27769  clwwisshclwwsn  27788  clwwlknon1sn  27873  frgr2wwlkeu  28100  frgrreg  28167  frgrregord013  28168  nvmul0or  28421  ubthlem3  28643  axhcompl-zf  28769  hvmul0or  28796  ocnel  29069  pjhthmo  29073  spanuni  29315  spansni  29328  hon0  29564  leopadd  29903  leoptr  29908  mdsymlem6  30179  sumdmdlem2  30190  cdjreui  30203  iundisj2f  30334  disjunsn  30338  iundisj2fi  30514  prmdvdsbc  30526  ballotlemimin  31758  bnj23  31983  bnj594  32179  bnj849  32192  cusgr3cyclex  32378  txsconn  32483  cvmsdisj  32512  cvmliftlem15  32540  cvmlift2lem10  32554  cvmlift3lem7  32567  fmla1  32629  satffunlem1lem2  32645  satffunlem2lem2  32648  mclsppslem  32825  dfon2lem3  33025  dfon2lem5  33027  dfon2lem6  33028  dfon2lem7  33029  dfon2lem8  33030  soseq  33091  frr3g  33116  noprefixmo  33197  noetalem3  33214  ifscgr  33500  cgr3tr4  33508  btwnconn1lem13  33555  seglecgr12  33567  elicc3  33660  neibastop1  33702  tailfb  33720  bj-sblem2  34162  bj-sngltag  34290  copsex2d  34425  mptsnunlem  34613  finxpreclem6  34671  wl-equsal1i  34777  lindsenlbs  34881  poimirlem26  34912  poimirlem27  34913  ismblfin  34927  itg2addnclem3  34939  ftc1anclem6  34966  fdc  35014  riscer  35260  intidl  35301  ispridlc  35342  prtlem14  36004  prtlem17  36006  lpssat  36143  lssatle  36145  lshpkrlem6  36245  cvrnbtwn  36401  atlatmstc  36449  atlatle  36450  atlrelat1  36451  2at0mat0  36655  trlator0  37301  cdleme0moN  37355  cdlemn11pre  38340  dihord2pre  38355  dihmeetlem20N  38456  dochkrshp4  38519  lcfl6  38630  remulid2  39242  diophin  39362  diophun  39363  inaex  40626  pm10.57  40696  fnchoice  41279  ellimcabssub0  41890  fourierdlem81  42465  fourierdlem93  42477  2reuimp0  43306  fzopredsuc  43516  2ffzoeq  43521  iccpartlt  43577  ichnreuop  43627  prmdvdsfmtnof1lem1  43739  lighneallem4  43768  odd2prm2  43876  even3prm2  43877  sbgoldbst  43936  nnsum4primesevenALTV  43959  nzerooringczr  44336  ply1mulgsumlem1  44433  snlindsntor  44519  islininds2  44532  m1modmmod  44574  itschlc0xyqsol1  44746  2itscp  44761