Theorem sylanbrc 421

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  945  ecase2d  1392  sb2  1820  sbequ1  1821  sbidm  1904  eqeu  2996  euind  3013  reuind  3031  eldifd  3230  eqssd  3265  ssrabdv  3327  elind  3414  dcun  3637  opm  4372  issod  4462  ordsucim  4645  onintonm  4662  ordtri2or2exmidlem  4671  en2lp  4699  ordwe  4721  sosng  4846  sotri2  5183  sotri3  5184  relssdmrn  5306  funun  5420  fnsng  5426  fnprg  5434  fntpg  5435  fntp  5436  fununi  5447  imain  5461  fnco  5489  f00  5582  f1ss  5602  f1ssr  5603  f1ssres  5605  f1f1orn  5648  foimacnv  5655  foun  5656  fun11iun  5658  sefvex  5714  dff3im  5847  fmpt  5852  ffnfv  5860  fmpt2d  5864  ffvresb  5865  fprg  5892  foco2  5953  fcof1  5983  fcofo  5984  fcof1o  5989  fliftf  5999  isoini2  6019  f1oiso  6026  moriotass  6063  fnoprabg  6183  f1ocnvd  6286  f1o3d  6292  suppssov1  6293  1stcof  6391  2ndcof  6392  1stconst  6451  2ndconst  6452  fo2ndf  6457  f1o2ndf1  6458  f1od2  6465  suppssfvg  6497  smores2  6559  tfrlem5  6579  tfrlemibfn  6593  tfr1onlembfn  6609  tfri1dALT  6616  tfrcllembfn  6622  nntri2  6761  eroveu  6894  elixpsn  7011  dom2lem  7052  xpf1o  7138  fidifsnen  7166  finexdc  7201  elssdc  7203  unfidisj  7223  f1finf1o  7258  fidcenumlemrks  7264  sbthlemi9  7276  supeuti  7328  infeuti  7363  casef1  7424  caseinl  7425  caseinr  7426  difinfsnlem  7433  ctmlemr  7442  ctm  7443  ctssdclemn0  7444  ctssdccl  7445  ctssdc  7447  enumctlemm  7448  nnnninf  7460  nninfwlpoimlemg  7509  en2other2  7542  exmidfodomrlemim  7547  pw1if  7578  pw1nel3  7584  dftap2  7611  cc2lem  7626  cc4f  7629  addclpi  7688  mulclpi  7689  nnppipi  7704  recmulnqg  7752  enq0ref  7794  nqnq0pi  7799  genipv  7870  addclpr  7898  nqprxx  7907  prmuloc  7927  mulclpr  7933  distrlem1prl  7943  distrlem1pru  7944  ltexprlempr  7969  ltexprlemrl  7971  ltexprlemru  7973  lteupri  7978  recexprlempr  7993  cauappcvgprlemm  8006  cauappcvgprlemopl  8007  cauappcvgprlemlol  8008  cauappcvgprlemopu  8009  cauappcvgprlemupu  8010  cauappcvgprlemloc  8013  cauappcvgprlemcl  8014  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlem2  8021  caucvgprlemm  8029  caucvgprlemopl  8030  caucvgprlemlol  8031  caucvgprlemopu  8032  caucvgprlemupu  8033  caucvgprlemloc  8036  caucvgprlemcl  8037  caucvgprlemladdfu  8038  caucvgprlem2  8041  caucvgprprlemml  8055  caucvgprprlemmu  8056  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemupu  8061  caucvgprprlemloc  8064  caucvgprprlemcl  8065  caucvgprprlem2  8071  suplocexprlemex  8083  suplocsrlem  8169  elrealeu  8190  rereceu  8250  axpre-suploclemres  8262  negf1o  8703  aptap  8972  receuap  8993  divvalap  8998  cju  9285  nn0ge2m1nn  9610  nnnegz  9630  elnnz  9637  elnn0z  9640  peano2z  9663  nn0n0n1ge2  9698  msqznn  9729  eluzaddi  9932  eluzsubi  9933  uzind4  9971  supinfneg  9978  infsupneg  9979  elnn1uz2  9990  uz2mulcl  9991  divfnzn  10004  nnrp  10047  rpaddcl  10061  rpmulcl  10062  rpdivcl  10063  rpgecl  10066  ge0p1rp  10069  elrpd  10077  ge0addcl  10366  ge0mulcl  10367  ge0xaddcl  10368  icoshftf1o  10376  peano2fzr  10424  uzsubsubfz  10435  fzsplit2  10438  fzsplit3  10441  elfznn  10443  fzss1  10452  fzss2  10453  fzp1elp1  10465  elfz1b  10480  elfz0fzfz0  10516  fz0fzelfz0  10517  difelfznle  10525  elfzofz  10553  nn0p1elfzo  10577  fzosplitsnm1  10610  ubmelm1fzo  10627  fzofzp1b  10629  fzosplitsn  10634  zsupcllemstep  10645  zsupcl  10647  infssfzcldc  10652  infssfzledc  10653  exbtwnz  10668  flqge0nn0  10711  flqge1nn  10712  zmodcl  10764  modqmuladdnn0  10788  modsumfzodifsn  10816  frec2uzf1od  10826  frec2uzisod  10827  frecuzrdgrrn  10828  frec2uzrdg  10829  frecuzrdgrcl  10830  frecuzrdgtcl  10832  frecuzrdgsuc  10834  frecuzrdgrclt  10835  frecuzrdgfunlem  10839  frecuzrdgtclt  10841  frecuzrdgsuctlem  10843  uzennn  10856  seq3fveq2  10895  seqfveq2g  10897  monoord  10905  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemab  10922  iseqf1olemqf1o  10926  seq3f1olemqsumkj  10931  seq3f1olemqsumk  10932  seq3id2  10946  exp3val  10961  expcl2lemap  10971  expclzaplem  10983  expge0  10995  expge1  10996  zsqcl2  11037  bcval4  11173  bcn1  11179  bccl2  11189  hashennnuni  11201  hashunlem  11227  hashdifpr  11244  zfz1isolem1  11275  seq3coll  11277  iswrdiz  11294  ccatsymb  11353  ccatrn  11360  ccat2s1fvwd  11398  swrds1  11423  swrdccat2  11426  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccatin12lem3  11487  pfxccatin12  11488  pfxccat3  11489  pfxccat3a  11493  shftfn  11572  shftf  11578  recvguniq  11744  resqrexlemdecn  11761  rersqreu  11777  nn0abscl  11834  nnabscl  11849  abs2dif  11855  nn0maxcl  11974  climuni  12042  2clim  12050  climcn2  12058  summodclem2a  12131  fsum3  12137  fsum3cvg3  12146  fsumcl2lem  12148  fsumadd  12156  fisum0diag2  12197  fsummulc2  12198  fsumge0  12209  geolim2  12262  cvgratnnlemabsle  12277  cvgratz  12282  mertenslemi1  12285  prodmodclem3  12325  prodmodclem2a  12326  fprodeq0  12367  fprodge0  12387  eff2  12430  tanvalap  12458  zdvdsdc  12562  fzo0dvdseq  12607  oexpneg  12627  oddge22np1  12631  evennn02n  12632  evennn2n  12633  nno  12656  divalglemeunn  12671  divalglemex  12672  divalglemeuneg  12673  divalg  12674  bitsfzolem  12704  bitsinv1lem  12711  divgcdz  12731  bezoutlemmain  12758  bezoutlemmo  12766  bezoutlemeu  12767  bezoutlemle  12768  sqgcd  12789  uzwodc  12797  nninfctlemfo  12800  eucalgval2  12814  eucalglt  12818  lcmneg  12835  lcmgcdlem  12838  ncoprmgcdne1b  12850  prmind2  12881  prmdc  12891  sqnprm  12897  isprm5lem  12902  isprm5  12903  isprm6  12908  sqrt2irrlem  12922  pw2dvdseu  12929  sqpweven  12936  2sqpwodd  12937  sqrt2irrap  12941  qgt0numnn  12960  phicl2  12975  crth  12985  phimullem  12986  eulerthlem1  12988  eulerthlemh  12992  eulerthlemth  12993  hashgcdlem  12999  oddprm  13021  pythagtriplem6  13032  pythagtriplem11  13036  pythagtriplem13  13038  pythagtriplem19  13044  pclem0  13048  pcpremul  13055  pceu  13057  pc2dvds  13092  difsqpwdvds  13100  pcadd  13102  pockthlem  13118  pockthg  13119  1arith  13129  4sqlemffi  13158  4sqlem11  13163  4sqlem12  13164  4sqlem13m  13165  4sqlem14  13166  4sqlem17  13169  ballotfilemic  13233  ballotfilem1c  13234  ballotfilemrc  13257  ballotfilemth  13264  oddennn  13266  evenennn  13267  ennnfoneleminc  13285  ennnfonelemf1  13292  ennnfonelemen  13295  exmidunben  13300  ctinf  13304  ctiunctlemfo  13313  nninfdclemlt  13325  nninfdclemf1  13326  ptex  13601  imasaddfnlemg  13618  imasaddflemg  13620  mgmsscl  13664  sgrp0  13708  sgrp1  13709  hashfinmndnn  13728  ismndd  13733  mndpfo  13734  mhmf1o  13760  0mhm  13776  resmhm  13777  resmhm2  13778  resmhm2b  13779  mhmco  13780  gsumvallem2  13783  isgrpd2e  13808  grpinvf1o  13858  grpinvnzcl  13860  dfgrp3m  13887  mhmmnd  13902  ghmgrp  13904  mulgval  13908  mulgfng  13910  subgmulg  13974  issubg4m  13979  isnsg3  13993  nmzsubg  13996  ssnmz  13997  0nsg  14000  nsgid  14001  ghmnsgima  14054  ghmnsgpreima  14055  ghmf1  14059  kerf1ghm  14060  ghmf1o  14061  conjnmzb  14066  isabld  14085  cmnsubm  14095  ghmcmn  14114  ghmabl  14115  invghm  14116  gsumvalfi  14135  srgfcl  14260  srglmhm  14280  srgrmhm  14281  iscrngd  14330  ringsrg  14335  unitabl  14407  rhmf1o  14458  rhmco  14464  ringelnzr  14477  subrngringnsg  14496  subrgcrng  14516  subrgnzr  14533  resrhm  14539  unitrrg  14559  aprnzr  14582  aprlring  14583  drngnzr  14602  lssneln0  14694  rnglidlmsgrp  14817  quscrng  14853  expghmap  14925  mulgghm2  14926  znf1o  14969  znidom  14975  znidomb  14976  isassad  14994  psrbaglesuppg  15040  psrbagcon  15045  tgtopon  15150  distopon  15171  epttop  15174  resttopon  15255  resttopon2  15262  cnco  15305  lmss  15330  txtopon  15346  uptx  15358  txdis1cn  15362  hmeocnv  15391  hmeof1o2  15392  hmeores  15399  hmeoco  15400  idhmeo  15401  txhmeo  15403  txswaphmeo  15405  psmetxrge0  15416  isxmet2d  15432  metres2  15465  xmetresbl  15524  comet  15583  bdxmet  15585  bdmet  15586  tgioo  15638  mulc1cncf  15673  mulcncflem  15691  cnrehmeocntop  15694  cnopnap  15695  dedekindeu  15707  dedekindicclemicc  15716  ivthinclemlm  15718  ivthinclemum  15719  ivthinclemlopn  15720  ivthinclemlr  15721  ivthinclemuopn  15722  ivthinclemur  15723  ivthinclemloc  15725  ivthinc  15727  ivthreinc  15729  dvfgg  15772  dvcjbr  15792  dvcj  15793  dvfre  15794  elplyr  15824  plyreres  15848  rplogbval  16030  sgmnncl  16085  mpodvdsmulf1o  16087  mersenne  16094  perfectlem2  16097  lgsfcl2  16108  lgsval2lem  16112  lgsmod  16128  lgsdirprm  16136  lgsne0  16140  gausslemma2dlem0h  16158  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  gausslemma2dlem4  16166  lgseisenlem1  16172  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  lgsquad2lem2  16184  2sqlem8  16225  2sqlem9  16226  structiedg0val  16264  ausgrumgrien  16394  usgredgreu  16440  uspgredg2vtxeu  16442  uspgredg2v  16445  usgredg2v  16448  usgr1e  16465  subuhgr  16496  subupgr  16497  subumgr  16498  subusgr  16499  vdegp1aid  16538  trlres  16614  clwwlkbp  16619  clwwlkccatlem  16624  s2elclwwlknon2  16660  clwwlknonex2lem2  16662  clwwlknonex2e  16664  bj-charfundcALT  16818  bj-nnord  16967  bj-inf2vnlem1  16979  pwf1oexmid  17012  nnsf  17022  nninfall  17026  nninfself  17030  exmidsbthrlem  17041  qdencn  17046  alsd  17105  ralsd  17106  alseud  17141  ralseud  17142