Theorem syl5bir 246

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3g  298  oplem1  1057  nic-ax  1681  19.30  1889  19.33b  1893  necon1bd  2958  spc2d  3517  pssdifn0  4280  ralnralall  4430  disjss3  5052  somo  5505  frminex  5531  sofld  6050  ordelord  6235  unizlim  6330  f0rn0  6604  funopfv  6764  mpteqb  6837  fvrnressn  6976  funfvima  7046  fpropnf1  7079  fliftfun  7121  weniso  7163  tfinds  7638  tfindsg  7639  tfindes  7641  tfinds2  7642  findsg  7677  frxp  7893  suppssr  7938  rdgsucmptnf  8165  frsucmptn  8174  tz7.49  8181  om00  8303  oewordi  8319  iiner  8471  eroveu  8494  fsetexb  8545  undom  8733  sucdom2  8755  sdomdif  8794  php3  8832  pssnn  8846  unxpdomlem3  8884  fisseneq  8889  pssnnOLD  8895  ordunifi  8921  isfinite2  8929  fiint  8948  infssuni  8967  ixpfi2  8974  finsschain  8983  ordtypelem10  9143  wofib  9161  wemapsolem  9166  unxpwdom2  9204  inf3lem2  9244  cantnfp1lem3  9295  cantnfp1  9296  setind  9350  frr3g  9372  r1tr  9392  r1ordg  9394  rankelb  9440  rankxplim3  9497  updjudhf  9547  cardlim  9588  infxpenlem  9627  infxpenc2  9636  dfac5lem4  9740  dfac12k  9761  kmlem13  9776  sornom  9891  fin23lem25  9938  fin23lem21  9953  zorn2lem4  10113  iundom2g  10154  fpwwe2lem11  10255  fpwwe2lem12  10256  pwfseqlem4a  10275  eltsk2g  10365  inttsk  10388  tskord  10394  r1tskina  10396  grudomon  10431  arch  12087  zaddcl  12217  uzm1  12472  xrsupsslem  12897  xrinfmsslem  12898  fsequb  13548  fseqsupubi  13551  ssnn0fi  13558  seqf1o  13617  sq01  13792  ccatalpha  14150  swrdnd0  14222  repsdf2  14343  cshw1  14387  wrdl3s3  14529  rexanre  14910  rexuzre  14916  cau3lem  14918  o1co  15147  rlimcn3  15151  o1of2  15174  lo1add  15188  lo1mul  15189  climcau  15234  climbdd  15235  caucvgb  15243  summo  15281  isumltss  15412  mertenslem2  15449  prodmolem2  15497  prodmo  15498  dvdsaddre2b  15868  bitsfzolem  15993  bitsfzo  15994  bezoutlem4  16102  lcmfeq0b  16187  lcmfunsnlem2  16197  divgcdcoprmex  16223  prmind2  16242  2mulprm  16250  isprm5  16264  prm23ge5  16368  pcqmul  16406  pcadd  16442  prmreclem2  16470  prmreclem5  16473  mul4sq  16507  vdwmc2  16532  ramcl  16582  prmgaplem7  16610  prmlem1a  16660  setsstruct2  16727  divsfval  17052  iscatd2  17184  catpropd  17212  wunfunc  17405  wunfuncOLD  17406  cyccom  18610  gaorber  18702  psgneu  18898  lsmsubm  19042  pj1eu  19086  efgredlem  19137  qusabl  19250  cygablOLD  19276  cygctb  19277  lt6abl  19280  gsumval3eu  19289  dprdsubg  19411  ablfac1c  19458  pgpfac1  19467  dvdsrtr  19670  unitgrp  19685  drngmul0or  19788  lvecvs0or  20145  lspdisjb  20163  lspsolvlem  20179  lspprat  20190  lbsextlem2  20196  abvn0b  20340  domnchr  20497  znfld  20525  cygznlem3  20534  obselocv  20690  cpmatacl  21613  chfacfisf  21751  chfacfisfcpmat  21752  0ntr  21968  opnneiid  22023  restntr  22079  hausnei2  22250  nrmsep3  22252  cmpsub  22297  uncmp  22300  dfconn2  22316  cnconn  22319  1stcfb  22342  txuni2  22462  txbas  22464  ptbasin  22474  txcls  22501  txbasval  22503  txlly  22533  txnlly  22534  pthaus  22535  txlm  22545  tx1stc  22547  xkohaus  22550  isufil2  22805  ufileu  22816  cnpflfi  22896  txflf  22903  fclscf  22922  flimfnfcls  22925  alexsubb  22943  alexsubALTlem2  22945  alexsubALTlem4  22947  ptcmplem2  22950  ptcmplem3  22951  cnextcn  22964  qustgplem  23018  prdsmet  23268  blin2  23327  prdsbl  23389  nmolb  23615  tgqioo  23697  reconnlem2  23724  reconn  23725  lebnumlem3  23860  iscau4  24176  cmetcaulem  24185  iscmet3lem2  24189  bcthlem5  24225  minveclem3b  24325  pmltpc  24347  evthicc2  24357  ovolunlem2  24395  ovolicc2lem5  24418  mblsplit  24429  iundisj2  24446  volsup  24453  ioombl1lem4  24458  dyaddisj  24493  dyadmbllem  24496  i1faddlem  24590  itg10a  24608  itg1ge0a  24609  mbfi1flimlem  24620  mbfmullem  24623  itg2add  24657  rolle  24887  dvcvx  24917  itgsubst  24946  tdeglem4  24957  tdeglem4OLD  24958  ply1domn  25021  fta1b  25067  plyadd  25111  plymul  25112  coeeu  25119  vieta1  25205  aalioulem6  25230  ulmcaulem  25286  ulmcau  25287  ulmbdd  25290  ulmcn  25291  amgm  25873  mumullem2  26062  ppiublem1  26083  dchrfi  26136  dchrptlem2  26146  dchrptlem3  26147  dchrsum2  26149  lgsdchr  26236  lgsquad2lem2  26266  2sqlem5  26303  2sqb  26313  pntlemp  26491  ostthlem2  26509  ostth  26520  iscgrglt  26605  tgbtwnconn1  26666  colline  26740  lmimid  26885  axcontlem8  27062  axcontlem9  27063  eengtrkg  27077  numedglnl  27235  uhgr2edg  27296  uspgr2wlkeq  27733  wlkonl1iedg  27753  wlkdlem2  27771  pthdlem2  27855  clwlkclwwlklem2a4  28080  clwwisshclwwsn  28099  clwwlknon1sn  28183  frgr2wwlkeu  28410  frgrreg  28477  frgrregord013  28478  nvmul0or  28731  ubthlem3  28953  axhcompl-zf  29079  hvmul0or  29106  ocnel  29379  pjhthmo  29383  spanuni  29625  spansni  29638  hon0  29874  leopadd  30213  leoptr  30218  mdsymlem6  30489  sumdmdlem2  30500  cdjreui  30513  iundisj2f  30648  disjunsn  30652  iundisj2fi  30838  prmdvdsbc  30850  ballotlemimin  32184  bnj23  32409  bnj594  32605  bnj849  32618  cusgr3cyclex  32811  txsconn  32916  cvmsdisj  32945  cvmliftlem15  32973  cvmlift2lem10  32987  cvmlift3lem7  33000  fmla1  33062  satffunlem1lem2  33078  satffunlem2lem2  33081  mclsppslem  33258  dfon2lem3  33480  dfon2lem5  33482  dfon2lem6  33483  dfon2lem7  33484  dfon2lem8  33485  poxp2  33527  poxp3  33533  soseq  33540  nosupprefixmo  33640  noinfprefixmo  33641  noetasuplem4  33676  madebdaylemlrcut  33816  ifscgr  34083  cgr3tr4  34091  btwnconn1lem13  34138  seglecgr12  34150  elicc3  34243  neibastop1  34285  tailfb  34303  bj-sblem2  34764  bj-sngltag  34910  copsex2d  35045  mptsnunlem  35246  finxpreclem6  35304  wl-equsal1i  35439  lindsenlbs  35509  poimirlem26  35540  poimirlem27  35541  ismblfin  35555  itg2addnclem3  35567  ftc1anclem6  35592  fdc  35640  riscer  35883  intidl  35924  ispridlc  35965  prtlem14  36625  prtlem17  36627  lpssat  36764  lssatle  36766  lshpkrlem6  36866  cvrnbtwn  37022  atlatmstc  37070  atlatle  37071  atlrelat1  37072  2at0mat0  37276  trlator0  37922  cdleme0moN  37976  cdlemn11pre  38961  dihord2pre  38976  dihmeetlem20N  39077  dochkrshp4  39140  lcfl6  39251  remulid2  40123  diophin  40297  diophun  40298  inaex  41588  pm10.57  41662  fnchoice  42245  ellimcabssub0  42833  fourierdlem81  43403  fourierdlem93  43415  2reuimp0  44278  fzopredsuc  44488  2ffzoeq  44493  iccpartlt  44549  ichnreuop  44597  prmdvdsfmtnof1lem1  44709  lighneallem4  44735  odd2prm2  44843  even3prm2  44844  sbgoldbst  44903  nnsum4primesevenALTV  44926  nzerooringczr  45303  ply1mulgsumlem1  45400  snlindsntor  45485  islininds2  45498  m1modmmod  45540  itschlc0xyqsol1  45785  2itscp  45800  opnneir  45873  iscnrm3lem2  45901