Theorem sylanbrc 394

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylanbrc.1	|- ( ph -> ps )
sylanbrc.2	|- ( ph -> ch )
sylanbrc.3	|- ( th <-> ( ps /\ ch ) )

Assertion

Ref	Expression
sylanbrc	|- ( ph -> th )

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 |- ( ph -> ps )
2		sylanbrc.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 290	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylanbrc.3	. 2 |- ( th <-> ( ps /\ ch ) )
5	3, 4	sylibr 137	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sb2  1650  sbequ1  1651  sbidm  1731  eqeu  2711  euind  2728  reuind  2744  eldifd  2928  eqssd  2962  ssrabdv  3019  psstr  3049  sspsstr  3050  psssstr  3051  opm  3971  issod  4056  ordsucim  4226  onintonm  4243  ordtri2or2exmidlem  4251  en2lp  4278  ordwe  4300  sosng  4413  sotri2  4722  sotri3  4723  relssdmrn  4841  funun  4944  fnsng  4947  fnprg  4954  fntpg  4955  fntp  4956  fununi  4967  imain  4981  fnco  5007  f00  5081  f1ss  5097  f1ssr  5098  f1ssres  5099  f1f1orn  5137  foimacnv  5144  foun  5145  fun11iun  5147  sefvex  5196  dff3im  5312  foco2  5318  fmpt  5319  ffnfv  5323  fmpt2d  5327  ffvresb  5328  fprg  5346  fcof1  5423  fcofo  5424  fcof1o  5429  fliftf  5439  isoini2  5458  f1oiso  5465  moriotass  5496  fnoprabg  5602  f1ocnvd  5702  suppssfv  5708  suppssov1  5709  1stcof  5790  2ndcof  5791  1stconst  5842  2ndconst  5843  fo2ndf  5848  f1o2ndf1  5849  smores2  5909  tfrlem5  5930  tfrlemibfn  5942  nntri2  6073  eroveu  6197  dom2lem  6252  fidifsnen  6331  addclpi  6425  mulclpi  6426  nnppipi  6441  recmulnqg  6489  enq0ref  6531  nqnq0pi  6536  genipv  6607  addclpr  6635  nqprxx  6644  prmuloc  6664  mulclpr  6670  distrlem1prl  6680  distrlem1pru  6681  ltexprlempr  6706  ltexprlemrl  6708  ltexprlemru  6710  lteupri  6715  recexprlempr  6730  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemloc  6750  cauappcvgprlemcl  6751  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlem2  6758  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlem2  6778  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemupu  6798  caucvgprprlemloc  6801  caucvgprprlemcl  6802  caucvgprprlem2  6808  elrealeu  6906  rereceu  6963  receuap  7650  divvalap  7653  cju  7913  nn0ge2m1nn  8242  nnnegz  8248  elnnz  8255  elnn0z  8258  peano2z  8281  nn0n0n1ge2  8311  msqznn  8338  eluzaddi  8499  eluzsubi  8500  uzind4  8531  elnn1uz2  8544  uz2mulcl  8545  divfnzn  8556  nnrp  8592  rpaddcl  8606  rpmulcl  8607  rpdivcl  8608  rpgecl  8611  ge0p1rp  8614  elrpd  8620  ge0addcl  8850  ge0mulcl  8851  icoshftf1o  8859  peano2fzr  8901  uzsubsubfz  8911  fzsplit2  8914  elfznn  8918  fzss1  8926  fzss2  8927  fzp1elp1  8937  elfz1b  8952  elfz0fzfz0  8983  fz0fzelfz0  8984  difelfznle  8993  elfzofz  9018  fzosplitsnm1  9065  ubmelm1fzo  9082  fzofzp1b  9084  fzosplitsn  9089  qbtwnz  9106  flqge0nn0  9135  flqge1nn  9136  frec2uzf1od  9192  frec2uzisod  9193  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgrom  9196  frecuzrdgfn  9198  frecuzrdgsuc  9201  iseqf  9224  iseqfveq2  9228  monoord  9235  serige0  9252  expival  9257  expcl2lemap  9267  expclzaplem  9279  expge0  9291  expge1  9292  zsqcl2  9331  shftfn  9425  shftf  9431  recvguniq  9593  resqrexlemdecn  9610  rersqreu  9626  nn0abscl  9681  nnabscl  9696  abs2dif  9702  climuni  9814  2clim  9822  climcn2  9830  sqr2irrlem  9877  bj-nnord  10083  bj-inf2vnlem1  10095  qdencn  10124