Theorem sylanbrc 408

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

Hypotheses

Ref	Expression
sylanbrc.1	⊢ (𝜑 → 𝜓)
sylanbrc.2	⊢ (𝜑 → 𝜒)
sylanbrc.3	⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
sylanbrc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylanbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 300	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylanbrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	3, 4	sylibr 132	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sb2  1690  sbequ1  1691  sbidm  1772  eqeu  2762  euind  2779  reuind  2795  eldifd  2983  eqssd  3016  ssrabdv  3073  opm  3989  issod  4074  ordsucim  4244  onintonm  4261  ordtri2or2exmidlem  4269  en2lp  4297  ordwe  4318  sosng  4431  sotri2  4742  sotri3  4743  relssdmrn  4861  funun  4964  fnsng  4967  fnprg  4974  fntpg  4975  fntp  4976  fununi  4987  imain  5001  fnco  5027  f00  5101  f1ss  5117  f1ssr  5118  f1ssres  5119  f1f1orn  5157  foimacnv  5164  foun  5165  fun11iun  5167  sefvex  5216  dff3im  5333  foco2  5339  fmpt  5340  ffnfv  5344  fmpt2d  5348  ffvresb  5349  fprg  5367  fcof1  5443  fcofo  5444  fcof1o  5449  fliftf  5459  isoini2  5478  f1oiso  5485  moriotass  5516  fnoprabg  5622  f1ocnvd  5722  suppssfv  5728  suppssov1  5729  1stcof  5810  2ndcof  5811  1stconst  5862  2ndconst  5863  fo2ndf  5868  f1o2ndf1  5869  f1od2  5876  smores2  5932  tfrlem5  5953  tfrlemibfn  5965  nntri2  6096  eroveu  6220  dom2lem  6275  fidifsnen  6355  supeuti  6407  infeuti  6442  addclpi  6517  mulclpi  6518  nnppipi  6533  recmulnqg  6581  enq0ref  6623  nqnq0pi  6628  genipv  6699  addclpr  6727  nqprxx  6736  prmuloc  6756  mulclpr  6762  distrlem1prl  6772  distrlem1pru  6773  ltexprlempr  6798  ltexprlemrl  6800  ltexprlemru  6802  lteupri  6807  recexprlempr  6822  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemupu  6839  cauappcvgprlemloc  6842  cauappcvgprlemcl  6843  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlem2  6850  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemupu  6862  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlem2  6870  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemupu  6890  caucvgprprlemloc  6893  caucvgprprlemcl  6894  caucvgprprlem2  6900  elrealeu  6998  rereceu  7055  negf1o  7486  receuap  7759  divvalap  7762  cju  8038  nn0ge2m1nn  8348  nnnegz  8354  elnnz  8361  elnn0z  8364  peano2z  8387  nn0n0n1ge2  8418  msqznn  8447  eluzaddi  8645  eluzsubi  8646  uzind4  8676  supinfneg  8683  infsupneg  8684  elnn1uz2  8694  uz2mulcl  8695  divfnzn  8706  nnrp  8743  rpaddcl  8757  rpmulcl  8758  rpdivcl  8759  rpgecl  8762  ge0p1rp  8765  elrpd  8771  ge0addcl  9004  ge0mulcl  9005  icoshftf1o  9013  peano2fzr  9056  uzsubsubfz  9066  fzsplit2  9069  elfznn  9073  fzss1  9081  fzss2  9082  fzp1elp1  9092  elfz1b  9107  elfz0fzfz0  9137  fz0fzelfz0  9138  difelfznle  9146  elfzofz  9171  fzosplitsnm1  9218  ubmelm1fzo  9235  fzofzp1b  9237  fzosplitsn  9242  qbtwnz  9260  flqge0nn0  9295  flqge1nn  9296  zmodcl  9346  modqmuladdnn0  9370  modsumfzodifsn  9398  frec2uzf1od  9408  frec2uzisod  9409  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgrom  9412  frecuzrdgfn  9414  frecuzrdgsuc  9417  iseqf  9444  iseqfveq2  9448  monoord  9455  serige0  9473  expival  9478  expcl2lemap  9488  expclzaplem  9500  expge0  9512  expge1  9513  zsqcl2  9553  bcval4  9679  bcn1  9685  bccl2  9695  shftfn  9712  shftf  9718  recvguniq  9881  resqrexlemdecn  9898  rersqreu  9914  nn0abscl  9971  nnabscl  9986  abs2dif  9992  climuni  10132  2clim  10140  climcn2  10148  zdvdsdc  10216  fzo0dvdseq  10257  oexpneg  10276  oddge22np1  10281  evennn02n  10282  evennn2n  10283  nno  10306  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  divalg  10324  zsupcllemstep  10341  zsupcl  10343  divgcdz  10363  bezoutlemmain  10387  bezoutlemmo  10395  bezoutlemeu  10396  bezoutlemle  10397  sqgcd  10418  eucalgval2  10435  eucalglt  10439  lcmcllem  10449  lcmledvds  10452  lcmneg  10456  lcmgcdlem  10459  ncoprmgcdne1b  10471  prmind2  10502  sqnprm  10517  isprm6  10526  sqrt2irrlem  10540  pw2dvdseu  10546  sqpweven  10553  2sqpwodd  10554  sqrt2irrap  10558  bj-nnord  10753  bj-inf2vnlem1  10765  qdencn  10785