Theorem sylanbrc 414

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 304	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylanbrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	3, 4	sylibr 133	1 ⊢ (𝜑 → 𝜃)

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sb2  1755  sbequ1  1756  sbidm  1839  eqeu  2896  euind  2913  reuind  2931  eldifd  3126  eqssd  3159  ssrabdv  3221  elind  3307  dcun  3519  opm  4212  issod  4297  ordsucim  4477  onintonm  4494  ordtri2or2exmidlem  4503  en2lp  4531  ordwe  4553  sosng  4677  sotri2  5001  sotri3  5002  relssdmrn  5124  funun  5232  fnsng  5235  fnprg  5243  fntpg  5244  fntp  5245  fununi  5256  imain  5270  fnco  5296  f00  5379  f1ss  5399  f1ssr  5400  f1ssres  5402  f1f1orn  5443  foimacnv  5450  foun  5451  fun11iun  5453  sefvex  5507  dff3im  5630  fmpt  5635  ffnfv  5643  fmpt2d  5647  ffvresb  5648  fprg  5668  foco2  5722  fcof1  5751  fcofo  5752  fcof1o  5757  fliftf  5767  isoini2  5787  f1oiso  5794  moriotass  5826  fnoprabg  5943  f1ocnvd  6040  suppssfv  6046  suppssov1  6047  1stcof  6131  2ndcof  6132  1stconst  6189  2ndconst  6190  fo2ndf  6195  f1o2ndf1  6196  f1od2  6203  smores2  6262  tfrlem5  6282  tfrlemibfn  6296  tfr1onlembfn  6312  tfri1dALT  6319  tfrcllembfn  6325  nntri2  6462  eroveu  6592  elixpsn  6701  dom2lem  6738  xpf1o  6810  fidifsnen  6836  finexdc  6868  unfidisj  6887  f1finf1o  6912  fidcenumlemrks  6918  sbthlemi9  6930  supeuti  6959  infeuti  6994  casef1  7055  caseinl  7056  caseinr  7057  difinfsnlem  7064  ctmlemr  7073  ctm  7074  ctssdclemn0  7075  ctssdccl  7076  ctssdc  7078  enumctlemm  7079  nnnninf  7090  en2other2  7152  exmidfodomrlemim  7157  pw1nel3  7187  cc2lem  7207  cc4f  7210  addclpi  7268  mulclpi  7269  nnppipi  7284  recmulnqg  7332  enq0ref  7374  nqnq0pi  7379  genipv  7450  addclpr  7478  nqprxx  7487  prmuloc  7507  mulclpr  7513  distrlem1prl  7523  distrlem1pru  7524  ltexprlempr  7549  ltexprlemrl  7551  ltexprlemru  7553  lteupri  7558  recexprlempr  7573  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemupu  7590  cauappcvgprlemloc  7593  cauappcvgprlemcl  7594  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlem2  7601  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemupu  7613  caucvgprlemloc  7616  caucvgprlemcl  7617  caucvgprlemladdfu  7618  caucvgprlem2  7621  caucvgprprlemml  7635  caucvgprprlemmu  7636  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemupu  7641  caucvgprprlemloc  7644  caucvgprprlemcl  7645  caucvgprprlem2  7651  suplocexprlemex  7663  suplocsrlem  7749  elrealeu  7770  rereceu  7830  axpre-suploclemres  7842  negf1o  8280  receuap  8566  divvalap  8570  cju  8856  nn0ge2m1nn  9174  nnnegz  9194  elnnz  9201  elnn0z  9204  peano2z  9227  nn0n0n1ge2  9261  msqznn  9291  eluzaddi  9492  eluzsubi  9493  uzind4  9526  supinfneg  9533  infsupneg  9534  elnn1uz2  9545  uz2mulcl  9546  divfnzn  9559  nnrp  9599  rpaddcl  9613  rpmulcl  9614  rpdivcl  9615  rpgecl  9618  ge0p1rp  9621  elrpd  9629  ge0addcl  9917  ge0mulcl  9918  ge0xaddcl  9919  icoshftf1o  9927  peano2fzr  9972  uzsubsubfz  9982  fzsplit2  9985  elfznn  9989  fzss1  9998  fzss2  9999  fzp1elp1  10010  elfz1b  10025  elfz0fzfz0  10061  fz0fzelfz0  10062  difelfznle  10070  elfzofz  10097  fzosplitsnm1  10144  ubmelm1fzo  10161  fzofzp1b  10163  fzosplitsn  10168  exbtwnz  10186  flqge0nn0  10228  flqge1nn  10229  zmodcl  10279  modqmuladdnn0  10303  modsumfzodifsn  10331  frec2uzf1od  10341  frec2uzisod  10342  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgtcl  10347  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgfunlem  10354  frecuzrdgtclt  10356  frecuzrdgsuctlem  10358  uzennn  10371  seq3fveq2  10404  monoord  10411  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemab  10424  iseqf1olemqf1o  10428  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3id2  10444  exp3val  10457  expcl2lemap  10467  expclzaplem  10479  expge0  10491  expge1  10492  zsqcl2  10532  bcval4  10665  bcn1  10671  bccl2  10681  hashennnuni  10692  hashunlem  10717  hashdifpr  10733  zfz1isolem1  10753  seq3coll  10755  shftfn  10766  shftf  10772  recvguniq  10937  resqrexlemdecn  10954  rersqreu  10970  nn0abscl  11027  nnabscl  11042  abs2dif  11048  climuni  11234  2clim  11242  climcn2  11250  summodclem2a  11322  fsum3  11328  fsum3cvg3  11337  fsumcl2lem  11339  fsumadd  11347  fisum0diag2  11388  fsummulc2  11389  fsumge0  11400  geolim2  11453  cvgratnnlemabsle  11468  cvgratz  11473  mertenslemi1  11476  prodmodclem3  11516  prodmodclem2a  11517  fprodeq0  11558  fprodge0  11578  eff2  11621  tanvalap  11649  zdvdsdc  11752  fzo0dvdseq  11795  oexpneg  11814  oddge22np1  11818  evennn02n  11819  evennn2n  11820  nno  11843  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  divalg  11861  zsupcllemstep  11878  zsupcl  11880  divgcdz  11904  bezoutlemmain  11931  bezoutlemmo  11939  bezoutlemeu  11940  bezoutlemle  11941  sqgcd  11962  uzwodc  11970  eucalgval2  11985  eucalglt  11989  lcmcllem  11999  lcmledvds  12002  lcmneg  12006  lcmgcdlem  12009  ncoprmgcdne1b  12021  prmind2  12052  prmdc  12062  sqnprm  12068  isprm5lem  12073  isprm5  12074  isprm6  12079  sqrt2irrlem  12093  pw2dvdseu  12100  sqpweven  12107  2sqpwodd  12108  sqrt2irrap  12112  qgt0numnn  12131  phicl2  12146  hashdvds  12153  crth  12156  phimullem  12157  eulerthlem1  12159  eulerthlemh  12163  eulerthlemth  12164  hashgcdlem  12170  oddprm  12191  pythagtriplem6  12202  pythagtriplem11  12206  pythagtriplem13  12208  pythagtriplem19  12214  pclem0  12218  pcpremul  12225  pceu  12227  pc2dvds  12261  difsqpwdvds  12269  pcadd  12271  pockthlem  12286  pockthg  12287  1arith  12297  oddennn  12325  evenennn  12326  ennnfoneleminc  12344  ennnfonelemf1  12351  ennnfonelemen  12354  exmidunben  12359  ctinf  12363  ctiunctlemfo  12372  nninfdclemlt  12384  nninfdclemf1  12385  mgmsscl  12592  tgtopon  12706  distopon  12727  epttop  12730  resttopon  12811  resttopon2  12818  cnco  12861  lmss  12886  txtopon  12902  uptx  12914  txdis1cn  12918  hmeocnv  12947  hmeof1o2  12948  hmeores  12955  hmeoco  12956  idhmeo  12957  txhmeo  12959  txswaphmeo  12961  psmetxrge0  12972  isxmet2d  12988  metres2  13021  xmetresbl  13080  comet  13139  bdxmet  13141  bdmet  13142  tgioo  13186  mulc1cncf  13216  mulcncflem  13230  cnrehmeocntop  13233  cnopnap  13234  dedekindeu  13241  dedekindicclemicc  13250  ivthinclemlm  13252  ivthinclemum  13253  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemloc  13259  ivthinc  13261  dvfgg  13297  dvcjbr  13312  dvcj  13313  dvfre  13314  rplogbval  13503  lgsfcl2  13547  lgsval2lem  13551  lgsmod  13567  lgsdirprm  13575  lgsne0  13579  2sqlem8  13599  2sqlem9  13600  bj-charfundcALT  13691  bj-nnord  13840  bj-inf2vnlem1  13852  pwf1oexmid  13879  nnsf  13885  nninfall  13889  nninfself  13893  exmidsbthrlem  13901  qdencn  13906