Theorem syl5bir 244

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr3g  296  oplem1  1047  nic-ax  1653  19.30  1861  19.33b  1865  necon1bd  3000  spc2d  3540  pssdifn0  4239  ralnralall  4366  disjss3  4955  somo  5390  frminex  5415  sofld  5912  ordelord  6080  unizlim  6174  f0rn0  6424  funopfv  6577  mpteqb  6644  fvrnressn  6777  funfvima  6849  fpropnf1  6881  fliftfun  6919  weniso  6961  tfinds  7421  tfindsg  7422  tfindes  7424  tfinds2  7425  findsg  7456  frxp  7664  suppssr  7703  rdgsucmptnf  7908  frsucmptn  7917  tz7.49  7923  om00  8042  oewordi  8058  iiner  8210  eroveu  8233  undom  8442  sdomdif  8502  php3  8540  sucdom2  8550  unxpdomlem3  8560  fisseneq  8565  pssnn  8572  ordunifi  8604  isfinite2  8612  fiint  8631  infssuni  8651  ixpfi2  8658  finsschain  8667  ordtypelem10  8827  wofib  8845  wemapsolem  8850  unxpwdom2  8888  inf3lem2  8927  cantnfp1lem3  8978  cantnfp1  8979  setind  9011  r1tr  9040  r1ordg  9042  rankelb  9088  rankxplim3  9145  updjudhf  9195  cardlim  9236  infxpenlem  9274  infxpenc2  9283  dfac5lem4  9387  dfac12k  9408  kmlem13  9423  sornom  9534  fin23lem25  9581  fin23lem21  9596  zorn2lem4  9756  iundom2g  9797  fpwwe2lem12  9898  fpwwe2lem13  9899  pwfseqlem4a  9918  eltsk2g  10008  inttsk  10031  tskord  10037  r1tskina  10039  grudomon  10074  arch  11731  zaddcl  11860  uzm1  12114  xrsupsslem  12539  xrinfmsslem  12540  fsequb  13181  fseqsupubi  13184  ssnn0fi  13191  seqf1o  13249  sq01  13424  ccatalpha  13779  ccat1st1st  13814  swrdnd0  13843  swrdccatin1  13911  repsdf2  13964  cshw1  14008  wrdl3s3  14148  rexanre  14528  rexuzre  14534  cau3lem  14536  o1co  14765  rlimcn2  14769  o1of2  14791  lo1add  14805  lo1mul  14806  climcau  14849  climbdd  14850  caucvgb  14858  summo  14895  isumltss  15024  mertenslem2  15062  prodmolem2  15110  prodmo  15111  dvdsaddre2b  15478  bitsfzolem  15604  bitsfzo  15605  bezoutlem4  15707  lcmfeq0b  15791  lcmfunsnlem2  15801  divgcdcoprmex  15827  prmind2  15846  2mulprm  15854  isprm5  15868  prm23ge5  15969  pcqmul  16007  pcadd  16042  prmreclem2  16070  prmreclem5  16073  mul4sq  16107  vdwmc2  16132  ramcl  16182  prmgaplem7  16210  prmlem1a  16257  setsstruct2  16338  divsfval  16637  iscatd2  16769  catpropd  16796  wunfunc  16986  gaorber  18167  psgneu  18353  lsmsubm  18496  pj1eu  18537  efgredlem  18588  qusabl  18696  cygabl  18720  cygctb  18721  lt6abl  18724  gsumval3eu  18733  dprdsubg  18851  ablfac1c  18898  pgpfac1  18907  dvdsrtr  19080  unitgrp  19095  drngmul0or  19201  lvecvs0or  19558  lspdisjb  19576  lspsolvlem  19592  lspprat  19603  lbsextlem2  19609  abvn0b  19752  domnchr  20349  znfld  20377  cygznlem3  20386  obselocv  20542  cpmatacl  20996  chfacfisf  21134  chfacfisfcpmat  21135  0ntr  21351  opnneiid  21406  restntr  21462  hausnei2  21633  nrmsep3  21635  cmpsub  21680  uncmp  21683  dfconn2  21699  cnconn  21702  1stcfb  21725  txuni2  21845  txbas  21847  ptbasin  21857  txcls  21884  txbasval  21886  txlly  21916  txnlly  21917  pthaus  21918  txlm  21928  tx1stc  21930  xkohaus  21933  isufil2  22188  ufileu  22199  cnpflfi  22279  txflf  22286  fclscf  22305  flimfnfcls  22308  alexsubb  22326  alexsubALTlem2  22328  alexsubALTlem4  22330  ptcmplem2  22333  ptcmplem3  22334  cnextcn  22347  qustgplem  22400  prdsmet  22651  blin2  22710  prdsbl  22772  nmolb  22997  tgqioo  23079  reconnlem2  23106  reconn  23107  lebnumlem3  23238  iscau4  23553  cmetcaulem  23562  iscmet3lem2  23566  bcthlem5  23602  minveclem3b  23702  pmltpc  23722  evthicc2  23732  ovolunlem2  23770  ovolicc2lem5  23793  mblsplit  23804  iundisj2  23821  volsup  23828  ioombl1lem4  23833  dyaddisj  23868  dyadmbllem  23871  i1faddlem  23965  itg10a  23982  itg1ge0a  23983  mbfi1flimlem  23994  mbfmullem  23997  itg2add  24031  rolle  24258  dvcvx  24288  itgsubst  24317  tdeglem4  24325  ply1domn  24388  fta1b  24434  plyadd  24478  plymul  24479  coeeu  24486  vieta1  24572  aalioulem6  24597  ulmcaulem  24653  ulmcau  24654  ulmbdd  24657  ulmcn  24658  amgm  25238  mumullem2  25427  ppiublem1  25448  dchrfi  25501  dchrptlem2  25511  dchrptlem3  25512  dchrsum2  25514  lgsdchr  25601  lgsquad2lem2  25631  2sqlem5  25668  2sqb  25678  pntlemp  25856  ostthlem2  25874  ostth  25885  iscgrglt  25970  tgbtwnconn1  26031  colline  26105  lmimid  26250  axcontlem8  26428  axcontlem9  26429  eengtrkg  26443  numedglnl  26600  uhgr2edg  26661  uspgr2wlkeq  27098  wlkonl1iedg  27117  wlkdlem2  27138  pthdlem2  27224  clwlkclwwlklem2a4  27450  clwwisshclwwsn  27469  clwwlknon1sn  27554  frgr2wwlkeu  27786  frgrreg  27853  frgrregord013  27854  nvmul0or  28106  ubthlem3  28328  axhcompl-zf  28454  hvmul0or  28481  ocnel  28754  pjhthmo  28758  spanuni  29000  spansni  29013  hon0  29249  leopadd  29588  leoptr  29593  mdsymlem6  29864  sumdmdlem2  29875  cdjreui  29888  iundisj2f  30006  disjunsn  30010  iundisj2fi  30178  prmdvdsbc  30187  ballotlemimin  31336  bnj23  31561  bnj594  31756  bnj849  31769  cusgr3cyclex  31947  txsconn  32052  cvmsdisj  32081  cvmliftlem15  32109  cvmlift2lem10  32123  cvmlift3lem7  32136  fmla1  32196  satffunlem1lem2  32211  satffunlem2lem2  32214  mclsppslem  32383  dfon2lem3  32583  dfon2lem5  32585  dfon2lem6  32586  dfon2lem7  32587  dfon2lem8  32588  soseq  32650  frr3g  32675  noprefixmo  32756  noetalem3  32773  ifscgr  33059  cgr3tr4  33067  btwnconn1lem13  33114  seglecgr12  33126  elicc3  33219  neibastop1  33261  tailfb  33279  bj-sblem2  33681  bj-sngltag  33846  bj-elid  33973  mptsnunlem  34096  finxpreclem6  34154  wl-equsal1i  34261  lindsenlbs  34364  poimirlem26  34395  poimirlem27  34396  ismblfin  34410  itg2addnclem3  34422  ftc1anclem6  34449  fdc  34498  riscer  34744  intidl  34785  ispridlc  34826  prtlem14  35491  prtlem17  35493  lpssat  35630  lssatle  35632  lshpkrlem6  35732  cvrnbtwn  35888  atlatmstc  35936  atlatle  35937  atlrelat1  35938  2at0mat0  36142  trlator0  36788  cdleme0moN  36842  cdlemn11pre  37827  dihord2pre  37842  dihmeetlem20N  37943  dochkrshp4  38006  lcfl6  38117  diophin  38805  diophun  38806  inaex  40082  pm10.57  40193  fnchoice  40777  ellimcabssub0  41394  fourierdlem81  41968  fourierdlem93  41980  2reuimp0  42783  fzopredsuc  42993  2ffzoeq  42998  iccpartlt  43020  ichnreuop  43070  prmdvdsfmtnof1lem1  43182  lighneallem4  43211  odd2prm2  43319  even3prm2  43320  sbgoldbst  43379  nnsum4primesevenALTV  43402  nzerooringczr  43775  ply1mulgsumlem1  43874  snlindsntor  43960  islininds2  43973  m1modmmod  44016  itschlc0xyqsol1  44188  2itscp  44203