Theorem sylanbrc 417

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  dcand  934  sb2  1778  sbequ1  1779  sbidm  1862  eqeu  2922  euind  2939  reuind  2957  eldifd  3154  eqssd  3187  ssrabdv  3249  elind  3335  dcun  3548  opm  4252  issod  4337  ordsucim  4517  onintonm  4534  ordtri2or2exmidlem  4543  en2lp  4571  ordwe  4593  sosng  4717  sotri2  5044  sotri3  5045  relssdmrn  5167  funun  5279  fnsng  5282  fnprg  5290  fntpg  5291  fntp  5292  fununi  5303  imain  5317  fnco  5343  f00  5426  f1ss  5446  f1ssr  5447  f1ssres  5449  f1f1orn  5491  foimacnv  5498  foun  5499  fun11iun  5501  sefvex  5555  dff3im  5682  fmpt  5687  ffnfv  5695  fmpt2d  5699  ffvresb  5700  fprg  5720  foco2  5775  fcof1  5805  fcofo  5806  fcof1o  5811  fliftf  5821  isoini2  5841  f1oiso  5848  moriotass  5880  fnoprabg  5997  f1ocnvd  6096  suppssfv  6102  suppssov1  6103  1stcof  6188  2ndcof  6189  1stconst  6246  2ndconst  6247  fo2ndf  6252  f1o2ndf1  6253  f1od2  6260  smores2  6319  tfrlem5  6339  tfrlemibfn  6353  tfr1onlembfn  6369  tfri1dALT  6376  tfrcllembfn  6382  nntri2  6519  eroveu  6652  elixpsn  6761  dom2lem  6798  xpf1o  6872  fidifsnen  6898  finexdc  6930  unfidisj  6950  f1finf1o  6976  fidcenumlemrks  6982  sbthlemi9  6994  supeuti  7023  infeuti  7058  casef1  7119  caseinl  7120  caseinr  7121  difinfsnlem  7128  ctmlemr  7137  ctm  7138  ctssdclemn0  7139  ctssdccl  7140  ctssdc  7142  enumctlemm  7143  nnnninf  7154  nninfwlpoimlemg  7203  en2other2  7225  exmidfodomrlemim  7230  pw1nel3  7260  dftap2  7280  cc2lem  7295  cc4f  7298  addclpi  7356  mulclpi  7357  nnppipi  7372  recmulnqg  7420  enq0ref  7462  nqnq0pi  7467  genipv  7538  addclpr  7566  nqprxx  7575  prmuloc  7595  mulclpr  7601  distrlem1prl  7611  distrlem1pru  7612  ltexprlempr  7637  ltexprlemrl  7639  ltexprlemru  7641  lteupri  7646  recexprlempr  7661  cauappcvgprlemm  7674  cauappcvgprlemopl  7675  cauappcvgprlemlol  7676  cauappcvgprlemopu  7677  cauappcvgprlemupu  7678  cauappcvgprlemloc  7681  cauappcvgprlemcl  7682  cauappcvgprlemladdfu  7683  cauappcvgprlemladdfl  7684  cauappcvgprlem2  7689  caucvgprlemm  7697  caucvgprlemopl  7698  caucvgprlemlol  7699  caucvgprlemopu  7700  caucvgprlemupu  7701  caucvgprlemloc  7704  caucvgprlemcl  7705  caucvgprlemladdfu  7706  caucvgprlem2  7709  caucvgprprlemml  7723  caucvgprprlemmu  7724  caucvgprprlemopl  7726  caucvgprprlemlol  7727  caucvgprprlemopu  7728  caucvgprprlemupu  7729  caucvgprprlemloc  7732  caucvgprprlemcl  7733  caucvgprprlem2  7739  suplocexprlemex  7751  suplocsrlem  7837  elrealeu  7858  rereceu  7918  axpre-suploclemres  7930  negf1o  8369  aptap  8637  receuap  8656  divvalap  8661  cju  8948  nn0ge2m1nn  9266  nnnegz  9286  elnnz  9293  elnn0z  9296  peano2z  9319  nn0n0n1ge2  9353  msqznn  9383  eluzaddi  9584  eluzsubi  9585  uzind4  9618  supinfneg  9625  infsupneg  9626  elnn1uz2  9637  uz2mulcl  9638  divfnzn  9651  nnrp  9693  rpaddcl  9707  rpmulcl  9708  rpdivcl  9709  rpgecl  9712  ge0p1rp  9715  elrpd  9723  ge0addcl  10011  ge0mulcl  10012  ge0xaddcl  10013  icoshftf1o  10021  peano2fzr  10067  uzsubsubfz  10077  fzsplit2  10080  elfznn  10084  fzss1  10093  fzss2  10094  fzp1elp1  10105  elfz1b  10120  elfz0fzfz0  10156  fz0fzelfz0  10157  difelfznle  10165  elfzofz  10192  fzosplitsnm1  10239  ubmelm1fzo  10256  fzofzp1b  10258  fzosplitsn  10263  exbtwnz  10281  flqge0nn0  10324  flqge1nn  10325  zmodcl  10375  modqmuladdnn0  10399  modsumfzodifsn  10427  frec2uzf1od  10437  frec2uzisod  10438  frecuzrdgrrn  10439  frec2uzrdg  10440  frecuzrdgrcl  10441  frecuzrdgtcl  10443  frecuzrdgsuc  10445  frecuzrdgrclt  10446  frecuzrdgfunlem  10450  frecuzrdgtclt  10452  frecuzrdgsuctlem  10454  uzennn  10467  seq3fveq2  10500  monoord  10507  iseqf1olemqcl  10517  iseqf1olemnab  10519  iseqf1olemab  10520  iseqf1olemqf1o  10524  seq3f1olemqsumkj  10529  seq3f1olemqsumk  10530  seq3id2  10540  exp3val  10553  expcl2lemap  10563  expclzaplem  10575  expge0  10587  expge1  10588  zsqcl2  10629  bcval4  10764  bcn1  10770  bccl2  10780  hashennnuni  10791  hashunlem  10816  hashdifpr  10832  zfz1isolem1  10852  seq3coll  10854  shftfn  10865  shftf  10871  recvguniq  11036  resqrexlemdecn  11053  rersqreu  11069  nn0abscl  11126  nnabscl  11141  abs2dif  11147  climuni  11333  2clim  11341  climcn2  11349  summodclem2a  11421  fsum3  11427  fsum3cvg3  11436  fsumcl2lem  11438  fsumadd  11446  fisum0diag2  11487  fsummulc2  11488  fsumge0  11499  geolim2  11552  cvgratnnlemabsle  11567  cvgratz  11572  mertenslemi1  11575  prodmodclem3  11615  prodmodclem2a  11616  fprodeq0  11657  fprodge0  11677  eff2  11720  tanvalap  11748  zdvdsdc  11851  fzo0dvdseq  11895  oexpneg  11914  oddge22np1  11918  evennn02n  11919  evennn2n  11920  nno  11943  divalglemeunn  11958  divalglemex  11959  divalglemeuneg  11960  divalg  11961  zsupcllemstep  11978  zsupcl  11980  divgcdz  12004  bezoutlemmain  12031  bezoutlemmo  12039  bezoutlemeu  12040  bezoutlemle  12041  sqgcd  12062  uzwodc  12070  eucalgval2  12085  eucalglt  12089  lcmneg  12106  lcmgcdlem  12109  ncoprmgcdne1b  12121  prmind2  12152  prmdc  12162  sqnprm  12168  isprm5lem  12173  isprm5  12174  isprm6  12179  sqrt2irrlem  12193  pw2dvdseu  12200  sqpweven  12207  2sqpwodd  12208  sqrt2irrap  12212  qgt0numnn  12231  phicl2  12246  hashdvds  12253  crth  12256  phimullem  12257  eulerthlem1  12259  eulerthlemh  12263  eulerthlemth  12264  hashgcdlem  12270  oddprm  12291  pythagtriplem6  12302  pythagtriplem11  12306  pythagtriplem13  12308  pythagtriplem19  12314  pclem0  12318  pcpremul  12325  pceu  12327  pc2dvds  12362  difsqpwdvds  12370  pcadd  12372  pockthlem  12388  pockthg  12389  1arith  12399  4sqlemffi  12428  4sqlem11  12433  4sqlem12  12434  4sqlem13m  12435  4sqlem14  12436  4sqlem17  12439  oddennn  12443  evenennn  12444  ennnfoneleminc  12462  ennnfonelemf1  12469  ennnfonelemen  12472  exmidunben  12477  ctinf  12481  ctiunctlemfo  12490  nninfdclemlt  12502  nninfdclemf1  12503  ptex  12769  imasaddfnlemg  12791  imasaddflemg  12793  mgmsscl  12837  sgrp0  12873  sgrp1  12874  hashfinmndnn  12893  ismndd  12898  mndpfo  12899  mhmf1o  12922  0mhm  12938  resmhm  12939  resmhm2  12940  resmhm2b  12941  mhmco  12942  isgrpd2e  12965  grpinvf1o  13014  grpinvnzcl  13016  dfgrp3m  13043  mhmmnd  13058  ghmgrp  13060  mulgval  13064  mulgfng  13066  subgmulg  13127  issubg4m  13132  isnsg3  13146  nmzsubg  13149  ssnmz  13150  0nsg  13153  nsgid  13154  ghmnsgima  13207  ghmnsgpreima  13208  ghmf1  13212  kerf1ghm  13213  ghmf1o  13214  conjnmzb  13219  isabld  13238  ghmcmn  13265  ghmabl  13266  srgfcl  13327  srglmhm  13347  srgrmhm  13348  iscrngd  13396  ringsrg  13399  unitabl  13467  rhmf1o  13518  rhmco  13524  ringelnzr  13534  subrngringnsg  13552  subrgcrng  13572  subrgnzr  13589  lssneln0  13690  rnglidlmsgrp  13813  quscrng  13847  mulgghm2  13906  psrbaglesuppg  13950  tgtopon  14023  distopon  14044  epttop  14047  resttopon  14128  resttopon2  14135  cnco  14178  lmss  14203  txtopon  14219  uptx  14231  txdis1cn  14235  hmeocnv  14264  hmeof1o2  14265  hmeores  14272  hmeoco  14273  idhmeo  14274  txhmeo  14276  txswaphmeo  14278  psmetxrge0  14289  isxmet2d  14305  metres2  14338  xmetresbl  14397  comet  14456  bdxmet  14458  bdmet  14459  tgioo  14503  mulc1cncf  14533  mulcncflem  14547  cnrehmeocntop  14550  cnopnap  14551  dedekindeu  14558  dedekindicclemicc  14567  ivthinclemlm  14569  ivthinclemum  14570  ivthinclemlopn  14571  ivthinclemlr  14572  ivthinclemuopn  14573  ivthinclemur  14574  ivthinclemloc  14576  ivthinc  14578  dvfgg  14614  dvcjbr  14629  dvcj  14630  dvfre  14631  rplogbval  14820  lgsfcl2  14865  lgsval2lem  14869  lgsmod  14885  lgsdirprm  14893  lgsne0  14897  lgseisenlem1  14908  lgseisenlem2  14909  2sqlem8  14928  2sqlem9  14929  bj-charfundcALT  15019  bj-nnord  15168  bj-inf2vnlem1  15180  pwf1oexmid  15208  nnsf  15213  nninfall  15217  nninfself  15221  exmidsbthrlem  15229  qdencn  15234