MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6ibr Unicode version

Theorem syl6ibr 219
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ibr.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6ibr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6ibr  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6ibr.2 . . 3  |-  ( th  <->  ch )
32biimpri 198 . 2  |-  ( ch 
->  th )
41, 3syl6 31 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr4g  262  imp4a  573  3impexpbicom  1373  nic-ax  1444  nfimd  1823  equs5eOLD  1907  ax12olem2  1973  ax12olem2OLD  1978  euim  2304  mopick2  2321  2moswap  2329  2eu1  2334  necon3ad  2603  necon3d  2605  necon1d  2636  ralrimd  2754  spcimegf  2990  spcegf  2992  spcimedv  2995  spc2gv  2999  spc3gv  3001  rspcimedv  3014  eqsbc3r  3178  ra5  3205  tpid3g  3879  pwpw0  3906  sssn  3917  pwsnALT  3970  ssiun  4093  ssiun2  4094  wefrc  4536  tron  4564  ordtri3or  4573  oneqmini  4592  reusv6OLD  4693  nnsuc  4821  dmcosseq  5096  relssres  5142  trin2  5216  ssrnres  5268  sossfld  5276  fnun  5510  f1oun  5653  brprcneu  5680  ssimaex  5747  chfnrn  5800  dffo4  5844  dffo5  5845  fvclss  5939  isomin  6016  isofrlem  6019  isoselem  6020  f1oweALT  6033  fnoprabg  6130  bropopvvv  6385  frxp  6415  poxp  6417  fnse  6422  mpt2xopynvov0g  6424  issmo2  6570  smores  6573  smogt  6588  rdglim2  6649  tz7.48lem  6657  tz7.49  6661  swoer  6892  qsss  6924  domtriord  7212  pssnn  7286  ssfi  7288  findcard  7306  findcard2  7307  findcard3  7309  frfi  7311  dffi3  7394  supmo  7413  inf3lem4  7542  carddom2  7820  fidomtri2  7837  pm54.43  7843  infpwfien  7899  alephordi  7911  cardaleph  7926  carduniima  7933  cardinfima  7934  alephval3  7947  dfac5lem4  7963  dfac5  7965  dfac2  7967  kmlem2  7987  cflm  8086  cfslb2n  8104  cfsmolem  8106  isf32lem9  8197  axcc4  8275  domtriomlem  8278  zorn2lem4  8335  zorn2lem6  8337  fpwwe2lem11  8471  fpwwe2lem12  8472  inttsk  8605  inar1  8606  intgru  8645  ingru  8646  indpi  8740  nqpr  8847  ltaddpr  8867  ltexprlem1  8869  ltexprlem5  8873  reclem2pr  8881  reclem4pr  8883  zmulcl  10280  uzm1  10472  uzwo  10495  uzwoOLD  10496  negn0  10518  xmullem2  10800  icoshft  10975  difreicc  10984  fzouzsplit  11123  seqf1olem1  11317  seqf1olem2  11318  hashtpg  11646  incexclem  12571  sqr2irr  12803  dvds2lem  12817  dvdslelem  12849  divalglem8  12875  euclemma  13063  iserodd  13164  ramcl  13352  mreiincl  13776  dirge  14637  sylow2alem1  15206  efgredlemb  15333  lbspss  16109  lspsneu  16150  lspsnat  16172  lspsncv0  16173  opsrtoslem2  16500  distop  17015  epttop  17028  isclo2  17107  restdis  17196  subbascn  17272  cnrest2  17304  cnpresti  17306  isnrm2  17376  cmpsublem  17416  cmpcld  17419  dfcon2  17435  t1conperf  17452  1stcrest  17469  lly1stc  17512  uptx  17610  txcn  17611  prdstopn  17613  txcon  17674  cmphaushmeo  17785  fbasrn  17869  csdfil  17879  trufil  17895  fclscf  18010  alexsubALTlem3  18033  alexsubALT  18035  haustsms2  18119  ovoliunlem1  19351  ovoliunnul  19356  volsup2  19450  coeaddlem  20120  plymul0or  20151  radcnv0  20285  wilthlem3  20806  chtub  20949  2sqlem10  21111  pntpbnd1  21233  usgrarnedg  21357  usgraedg4  21359  isch3  22697  shmodsi  22844  orthin  22901  h1datomi  23036  stcltr2i  23731  atom1d  23809  sumdmdii  23871  cdj3lem1  23890  disjpreima  23979  kerf1hrm  24215  lmxrge0  24290  dmvlsiga  24465  sibfof  24607  erdszelem9  24838  cvmlift2lem1  24942  fundmpss  25336  tfisg  25418  wfisg  25423  frinsg  25459  poseq  25467  sltval2  25524  nodenselem7  25555  nofulllem5  25574  mptelee  25738  axeuclidlem  25805  axcontlem4  25810  outsideofrflx  25965  mblfinlem2  26144  itg2addnclem3  26157  nn0prpwlem  26215  ivthALT  26228  fnessref  26263  neibastop2lem  26279  tailfb  26296  cover2  26305  fdc  26339  nninfnub  26345  equivtotbnd  26377  prdstotbnd  26393  cntotbnd  26395  ablo4pnp  26445  isdrngo3  26465  crngohomfo  26506  intidl  26529  prtlem90  26596  prtlem18  26616  prter2  26620  2reu1  27831  swrdnd  28001  swrdccatin12lem3c  28023  swrdccat3  28029  frgrancvvdeqlemA  28140  frgrancvvdeqlemC  28142  alrim3con13v  28328  tratrb  28331  onfrALTlem3  28341  onfrALTlem2  28343  onfrALTlem1  28345  trsspwALT2  28641  trsspwALT3  28642  bnj600  28996  bnj1018  29039  bnj1173  29077  bnj1174  29078  lsat0cv  29516  lfl1  29553  lkreqN  29653  atlrelat1  29804  pmaple  30243  pmapsub  30250  pclclN  30373  pclfinN  30382  osumcllem4N  30441  pexmidlem1N  30452  cdleme7ga  30730  lcfl7N  31984
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator