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  1694  sbequ1  1695  sbidm  1776  eqeu  2776  euind  2793  reuind  2809  eldifd  2998  eqssd  3031  ssrabdv  3089  elind  3174  opm  4037  issod  4122  ordsucim  4292  onintonm  4309  ordtri2or2exmidlem  4317  en2lp  4345  ordwe  4366  sosng  4481  sotri2  4798  sotri3  4799  relssdmrn  4919  funun  5025  fnsng  5028  fnprg  5036  fntpg  5037  fntp  5038  fununi  5049  imain  5063  fnco  5089  f00  5167  f1ss  5187  f1ssr  5188  f1ssres  5190  f1f1orn  5229  foimacnv  5236  foun  5237  fun11iun  5239  sefvex  5291  dff3im  5409  fmpt  5414  ffnfv  5421  fmpt2d  5425  ffvresb  5426  fprg  5445  foco2  5496  fcof1  5525  fcofo  5526  fcof1o  5531  fliftf  5541  isoini2  5561  f1oiso  5568  moriotass  5599  fnoprabg  5705  f1ocnvd  5805  suppssfv  5811  suppssov1  5812  1stcof  5893  2ndcof  5894  1stconst  5945  2ndconst  5946  fo2ndf  5951  f1o2ndf1  5952  f1od2  5959  smores2  6015  tfrlem5  6035  tfrlemibfn  6049  tfr1onlembfn  6065  tfri1dALT  6072  tfrcllembfn  6078  nntri2  6211  eroveu  6337  dom2lem  6443  xpf1o  6514  fidifsnen  6540  finexdc  6572  unfidisj  6586  f1finf1o  6608  sbthlemi9  6621  supeuti  6636  infeuti  6671  casef1  6728  nnnninf  6753  en2other2  6769  exmidfodomrlemim  6774  addclpi  6833  mulclpi  6834  nnppipi  6849  recmulnqg  6897  enq0ref  6939  nqnq0pi  6944  genipv  7015  addclpr  7043  nqprxx  7052  prmuloc  7072  mulclpr  7078  distrlem1prl  7088  distrlem1pru  7089  ltexprlempr  7114  ltexprlemrl  7116  ltexprlemru  7118  lteupri  7123  recexprlempr  7138  cauappcvgprlemm  7151  cauappcvgprlemopl  7152  cauappcvgprlemlol  7153  cauappcvgprlemopu  7154  cauappcvgprlemupu  7155  cauappcvgprlemloc  7158  cauappcvgprlemcl  7159  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlem2  7166  caucvgprlemm  7174  caucvgprlemopl  7175  caucvgprlemlol  7176  caucvgprlemopu  7177  caucvgprlemupu  7178  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlem2  7186  caucvgprprlemml  7200  caucvgprprlemmu  7201  caucvgprprlemopl  7203  caucvgprprlemlol  7204  caucvgprprlemopu  7205  caucvgprprlemupu  7206  caucvgprprlemloc  7209  caucvgprprlemcl  7210  caucvgprprlem2  7216  elrealeu  7314  rereceu  7371  negf1o  7807  receuap  8080  divvalap  8083  cju  8359  nn0ge2m1nn  8669  nnnegz  8689  elnnz  8696  elnn0z  8699  peano2z  8722  nn0n0n1ge2  8753  msqznn  8782  eluzaddi  8980  eluzsubi  8981  uzind4  9011  supinfneg  9018  infsupneg  9019  elnn1uz2  9029  uz2mulcl  9030  divfnzn  9041  nnrp  9078  rpaddcl  9092  rpmulcl  9093  rpdivcl  9094  rpgecl  9097  ge0p1rp  9100  elrpd  9106  ge0addcl  9334  ge0mulcl  9335  icoshftf1o  9343  peano2fzr  9386  uzsubsubfz  9396  fzsplit2  9399  elfznn  9403  fzss1  9411  fzss2  9412  fzp1elp1  9422  elfz1b  9437  elfz0fzfz0  9468  fz0fzelfz0  9469  difelfznle  9477  elfzofz  9504  fzosplitsnm1  9551  ubmelm1fzo  9568  fzofzp1b  9570  fzosplitsn  9575  exbtwnz  9593  flqge0nn0  9631  flqge1nn  9632  zmodcl  9682  modqmuladdnn0  9706  modsumfzodifsn  9734  frec2uzf1od  9744  frec2uzisod  9745  frecuzrdgrrn  9746  frec2uzrdg  9747  frecuzrdgrcl  9748  frecuzrdgtcl  9750  frecuzrdgsuc  9752  frecuzrdgrclt  9753  frecuzrdgfunlem  9757  frecuzrdgtclt  9759  frecuzrdgsuctlem  9761  iseqfveq2  9806  monoord  9813  iseqf1olemqcl  9823  iseqf1olemnab  9825  iseqf1olemab  9826  iseqf1olemqf1o  9830  iseqf1olemqsumkj  9835  iseqf1olemqsumk  9836  iseqid2  9847  serige0  9854  expival  9859  expcl2lemap  9869  expclzaplem  9881  expge0  9893  expge1  9894  zsqcl2  9934  bcval4  10060  bcn1  10066  bccl2  10076  hashennnuni  10087  hashunlem  10112  hashdifpr  10128  zfz1isolem1  10145  iseqcoll  10147  shftfn  10158  shftf  10164  recvguniq  10327  resqrexlemdecn  10344  rersqreu  10360  nn0abscl  10417  nnabscl  10432  abs2dif  10438  climuni  10579  2clim  10587  climcn2  10595  isummolem2a  10665  fisum  10670  fisumcvg3  10679  fsumcl2lem  10680  fsumadd  10688  zdvdsdc  10723  fzo0dvdseq  10764  oexpneg  10783  oddge22np1  10787  evennn02n  10788  evennn2n  10789  nno  10812  divalglemeunn  10827  divalglemex  10828  divalglemeuneg  10829  divalg  10830  zsupcllemstep  10847  zsupcl  10849  divgcdz  10869  bezoutlemmain  10893  bezoutlemmo  10901  bezoutlemeu  10902  bezoutlemle  10903  sqgcd  10924  eucalgval2  10941  eucalglt  10945  lcmcllem  10955  lcmledvds  10958  lcmneg  10962  lcmgcdlem  10965  ncoprmgcdne1b  10977  prmind2  11008  sqnprm  11023  isprm6  11032  sqrt2irrlem  11046  pw2dvdseu  11052  sqpweven  11059  2sqpwodd  11060  sqrt2irrap  11064  qgt0numnn  11083  phicl2  11096  hashdvds  11103  crth  11106  phimullem  11107  hashgcdlem  11109  oddennn  11111  evenennn  11112  bj-nnord  11322  bj-inf2vnlem1  11334  nnsf  11364  nninfall  11369  nninfself  11374  exmidsbthrlem  11381  qdencn  11384