Theorem syl5bir 242

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3g  294  oplem1  1053  nic-ax  1677  19.30  1885  19.33b  1889  necon1bd  2960  spc2d  3531  pssdifn0  4296  ralnralall  4446  disjss3  5069  somo  5531  frminex  5560  sofld  6079  predtrss  6214  ordelord  6273  unizlim  6368  f0rn0  6643  funopfv  6803  mpteqb  6876  fvrnressn  7015  funfvima  7088  fpropnf1  7121  fliftfun  7163  weniso  7205  tfinds  7681  tfindsg  7682  tfindes  7684  tfinds2  7685  findsg  7720  frxp  7938  suppssr  7983  rdgsucmptnf  8231  frsucmptn  8240  tz7.49  8246  om00  8368  oewordi  8384  iiner  8536  eroveu  8559  fsetexb  8610  undom  8800  sucdom2  8822  sdomdif  8861  php3  8899  pssnn  8913  unxpdomlem3  8958  fisseneq  8963  pssnnOLD  8969  ordunifi  8994  isfinite2  9002  fiint  9021  infssuni  9040  ixpfi2  9047  finsschain  9056  ordtypelem10  9216  wofib  9234  wemapsolem  9239  unxpwdom2  9277  inf3lem2  9317  cantnfp1lem3  9368  cantnfp1  9369  setind  9423  frr3g  9445  r1tr  9465  r1ordg  9467  rankelb  9513  rankxplim3  9570  updjudhf  9620  cardlim  9661  infxpenlem  9700  infxpenc2  9709  dfac5lem4  9813  dfac12k  9834  kmlem13  9849  sornom  9964  fin23lem25  10011  fin23lem21  10026  zorn2lem4  10186  iundom2g  10227  fpwwe2lem11  10328  fpwwe2lem12  10329  pwfseqlem4a  10348  eltsk2g  10438  inttsk  10461  tskord  10467  r1tskina  10469  grudomon  10504  arch  12160  zaddcl  12290  uzm1  12545  xrsupsslem  12970  xrinfmsslem  12971  fsequb  13623  fseqsupubi  13626  ssnn0fi  13633  seqf1o  13692  sq01  13868  ccatalpha  14226  swrdnd0  14298  repsdf2  14419  cshw1  14463  wrdl3s3  14605  rexanre  14986  rexuzre  14992  cau3lem  14994  o1co  15223  rlimcn3  15227  o1of2  15250  lo1add  15264  lo1mul  15265  climcau  15310  climbdd  15311  caucvgb  15319  summo  15357  isumltss  15488  mertenslem2  15525  prodmolem2  15573  prodmo  15574  dvdsaddre2b  15944  bitsfzolem  16069  bitsfzo  16070  bezoutlem4  16178  lcmfeq0b  16263  lcmfunsnlem2  16273  divgcdcoprmex  16299  prmind2  16318  2mulprm  16326  isprm5  16340  prm23ge5  16444  pcqmul  16482  pcadd  16518  prmreclem2  16546  prmreclem5  16549  mul4sq  16583  vdwmc2  16608  ramcl  16658  prmgaplem7  16686  prmlem1a  16736  setsstruct2  16803  divsfval  17175  iscatd2  17307  catpropd  17335  wunfunc  17530  wunfuncOLD  17531  cyccom  18737  gaorber  18829  psgneu  19029  lsmsubm  19173  pj1eu  19217  efgredlem  19268  qusabl  19381  cygablOLD  19407  cygctb  19408  lt6abl  19411  gsumval3eu  19420  dprdsubg  19542  ablfac1c  19589  pgpfac1  19598  dvdsrtr  19809  unitgrp  19824  drngmul0or  19927  lvecvs0or  20285  lspdisjb  20303  lspsolvlem  20319  lspprat  20330  lbsextlem2  20336  abvn0b  20486  domnchr  20648  znfld  20680  cygznlem3  20689  obselocv  20845  cpmatacl  21773  chfacfisf  21911  chfacfisfcpmat  21912  0ntr  22130  opnneiid  22185  restntr  22241  hausnei2  22412  nrmsep3  22414  cmpsub  22459  uncmp  22462  dfconn2  22478  cnconn  22481  1stcfb  22504  txuni2  22624  txbas  22626  ptbasin  22636  txcls  22663  txbasval  22665  txlly  22695  txnlly  22696  pthaus  22697  txlm  22707  tx1stc  22709  xkohaus  22712  isufil2  22967  ufileu  22978  cnpflfi  23058  txflf  23065  fclscf  23084  flimfnfcls  23087  alexsubb  23105  alexsubALTlem2  23107  alexsubALTlem4  23109  ptcmplem2  23112  ptcmplem3  23113  cnextcn  23126  qustgplem  23180  prdsmet  23431  blin2  23490  prdsbl  23553  nmolb  23787  tgqioo  23869  reconnlem2  23896  reconn  23897  lebnumlem3  24032  iscau4  24348  cmetcaulem  24357  iscmet3lem2  24361  bcthlem5  24397  minveclem3b  24497  pmltpc  24519  evthicc2  24529  ovolunlem2  24567  ovolicc2lem5  24590  mblsplit  24601  iundisj2  24618  volsup  24625  ioombl1lem4  24630  dyaddisj  24665  dyadmbllem  24668  i1faddlem  24762  itg10a  24780  itg1ge0a  24781  mbfi1flimlem  24792  mbfmullem  24795  itg2add  24829  rolle  25059  dvcvx  25089  itgsubst  25118  tdeglem4  25129  tdeglem4OLD  25130  ply1domn  25193  fta1b  25239  plyadd  25283  plymul  25284  coeeu  25291  vieta1  25377  aalioulem6  25402  ulmcaulem  25458  ulmcau  25459  ulmbdd  25462  ulmcn  25463  amgm  26045  mumullem2  26234  ppiublem1  26255  dchrfi  26308  dchrptlem2  26318  dchrptlem3  26319  dchrsum2  26321  lgsdchr  26408  lgsquad2lem2  26438  2sqlem5  26475  2sqb  26485  pntlemp  26663  ostthlem2  26681  ostth  26692  iscgrglt  26779  tgbtwnconn1  26840  colline  26914  lmimid  27059  axcontlem8  27242  axcontlem9  27243  eengtrkg  27257  numedglnl  27417  uhgr2edg  27478  uspgr2wlkeq  27915  wlkonl1iedg  27935  wlkdlem2  27953  pthdlem2  28037  clwlkclwwlklem2a4  28262  clwwisshclwwsn  28281  clwwlknon1sn  28365  frgr2wwlkeu  28592  frgrreg  28659  frgrregord013  28660  nvmul0or  28913  ubthlem3  29135  axhcompl-zf  29261  hvmul0or  29288  ocnel  29561  pjhthmo  29565  spanuni  29807  spansni  29820  hon0  30056  leopadd  30395  leoptr  30400  mdsymlem6  30671  sumdmdlem2  30682  cdjreui  30695  iundisj2f  30830  disjunsn  30834  iundisj2fi  31020  prmdvdsbc  31032  ballotlemimin  32372  bnj23  32597  bnj594  32792  bnj849  32805  cusgr3cyclex  32998  txsconn  33103  cvmsdisj  33132  cvmliftlem15  33160  cvmlift2lem10  33174  cvmlift3lem7  33187  fmla1  33249  satffunlem1lem2  33265  satffunlem2lem2  33268  mclsppslem  33445  dfon2lem3  33667  dfon2lem5  33669  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  poxp2  33717  poxp3  33723  soseq  33730  nosupprefixmo  33830  noinfprefixmo  33831  noetasuplem4  33866  madebdaylemlrcut  34006  ifscgr  34273  cgr3tr4  34281  btwnconn1lem13  34328  seglecgr12  34340  elicc3  34433  neibastop1  34475  tailfb  34493  bj-sblem2  34954  bj-sngltag  35100  copsex2d  35237  mptsnunlem  35436  finxpreclem6  35494  wl-equsal1i  35629  lindsenlbs  35699  poimirlem26  35730  poimirlem27  35731  ismblfin  35745  itg2addnclem3  35757  ftc1anclem6  35782  fdc  35830  riscer  36073  intidl  36114  ispridlc  36155  prtlem14  36815  prtlem17  36817  lpssat  36954  lssatle  36956  lshpkrlem6  37056  cvrnbtwn  37212  atlatmstc  37260  atlatle  37261  atlrelat1  37262  2at0mat0  37466  trlator0  38112  cdleme0moN  38166  cdlemn11pre  39151  dihord2pre  39166  dihmeetlem20N  39267  dochkrshp4  39330  lcfl6  39441  remulid2  40336  diophin  40510  diophun  40511  inaex  41804  pm10.57  41878  fnchoice  42461  ellimcabssub0  43048  fourierdlem81  43618  fourierdlem93  43630  2reuimp0  44493  fzopredsuc  44703  2ffzoeq  44708  iccpartlt  44764  ichnreuop  44812  prmdvdsfmtnof1lem1  44924  lighneallem4  44950  odd2prm2  45058  even3prm2  45059  sbgoldbst  45118  nnsum4primesevenALTV  45141  nzerooringczr  45518  ply1mulgsumlem1  45615  snlindsntor  45700  islininds2  45713  m1modmmod  45755  itschlc0xyqsol1  46000  2itscp  46015  opnneir  46088  iscnrm3lem2  46116