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  938  ecase2d  1385  sb2  1813  sbequ1  1814  sbidm  1897  eqeu  2973  euind  2990  reuind  3008  eldifd  3207  eqssd  3241  ssrabdv  3303  elind  3389  dcun  3601  opm  4320  issod  4410  ordsucim  4592  onintonm  4609  ordtri2or2exmidlem  4618  en2lp  4646  ordwe  4668  sosng  4792  sotri2  5126  sotri3  5127  relssdmrn  5249  funun  5362  fnsng  5368  fnprg  5376  fntpg  5377  fntp  5378  fununi  5389  imain  5403  fnco  5431  f00  5519  f1ss  5539  f1ssr  5540  f1ssres  5542  f1f1orn  5585  foimacnv  5592  foun  5593  fun11iun  5595  sefvex  5650  dff3im  5782  fmpt  5787  ffnfv  5795  fmpt2d  5799  ffvresb  5800  fprg  5826  foco2  5883  fcof1  5913  fcofo  5914  fcof1o  5919  fliftf  5929  isoini2  5949  f1oiso  5956  moriotass  5991  fnoprabg  6111  f1ocnvd  6214  suppssfv  6220  suppssov1  6221  1stcof  6315  2ndcof  6316  1stconst  6373  2ndconst  6374  fo2ndf  6379  f1o2ndf1  6380  f1od2  6387  smores2  6446  tfrlem5  6466  tfrlemibfn  6480  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  nntri2  6648  eroveu  6781  elixpsn  6890  dom2lem  6931  xpf1o  7013  fidifsnen  7040  finexdc  7072  unfidisj  7092  f1finf1o  7122  fidcenumlemrks  7128  sbthlemi9  7140  supeuti  7169  infeuti  7204  casef1  7265  caseinl  7266  caseinr  7267  difinfsnlem  7274  ctmlemr  7283  ctm  7284  ctssdclemn0  7285  ctssdccl  7286  ctssdc  7288  enumctlemm  7289  nnnninf  7301  nninfwlpoimlemg  7350  en2other2  7382  exmidfodomrlemim  7387  pw1if  7418  pw1nel3  7424  dftap2  7445  cc2lem  7460  cc4f  7463  addclpi  7522  mulclpi  7523  nnppipi  7538  recmulnqg  7586  enq0ref  7628  nqnq0pi  7633  genipv  7704  addclpr  7732  nqprxx  7741  prmuloc  7761  mulclpr  7767  distrlem1prl  7777  distrlem1pru  7778  ltexprlempr  7803  ltexprlemrl  7805  ltexprlemru  7807  lteupri  7812  recexprlempr  7827  cauappcvgprlemm  7840  cauappcvgprlemopl  7841  cauappcvgprlemlol  7842  cauappcvgprlemopu  7843  cauappcvgprlemupu  7844  cauappcvgprlemloc  7847  cauappcvgprlemcl  7848  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlem2  7855  caucvgprlemm  7863  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemopu  7866  caucvgprlemupu  7867  caucvgprlemloc  7870  caucvgprlemcl  7871  caucvgprlemladdfu  7872  caucvgprlem2  7875  caucvgprprlemml  7889  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemupu  7895  caucvgprprlemloc  7898  caucvgprprlemcl  7899  caucvgprprlem2  7905  suplocexprlemex  7917  suplocsrlem  8003  elrealeu  8024  rereceu  8084  axpre-suploclemres  8096  negf1o  8536  aptap  8805  receuap  8824  divvalap  8829  cju  9116  nn0ge2m1nn  9437  nnnegz  9457  elnnz  9464  elnn0z  9467  peano2z  9490  nn0n0n1ge2  9525  msqznn  9555  eluzaddi  9757  eluzsubi  9758  uzind4  9791  supinfneg  9798  infsupneg  9799  elnn1uz2  9810  uz2mulcl  9811  divfnzn  9824  nnrp  9867  rpaddcl  9881  rpmulcl  9882  rpdivcl  9883  rpgecl  9886  ge0p1rp  9889  elrpd  9897  ge0addcl  10185  ge0mulcl  10186  ge0xaddcl  10187  icoshftf1o  10195  peano2fzr  10241  uzsubsubfz  10251  fzsplit2  10254  elfznn  10258  fzss1  10267  fzss2  10268  fzp1elp1  10279  elfz1b  10294  elfz0fzfz0  10330  fz0fzelfz0  10331  difelfznle  10339  elfzofz  10367  fzosplitsnm1  10423  ubmelm1fzo  10440  fzofzp1b  10442  fzosplitsn  10447  zsupcllemstep  10457  zsupcl  10459  exbtwnz  10478  flqge0nn0  10521  flqge1nn  10522  zmodcl  10574  modqmuladdnn0  10598  modsumfzodifsn  10626  frec2uzf1od  10636  frec2uzisod  10637  frecuzrdgrrn  10638  frec2uzrdg  10639  frecuzrdgrcl  10640  frecuzrdgtcl  10642  frecuzrdgsuc  10644  frecuzrdgrclt  10645  frecuzrdgfunlem  10649  frecuzrdgtclt  10651  frecuzrdgsuctlem  10653  uzennn  10666  seq3fveq2  10705  seqfveq2g  10707  monoord  10715  iseqf1olemqcl  10729  iseqf1olemnab  10731  iseqf1olemab  10732  iseqf1olemqf1o  10736  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3id2  10756  exp3val  10771  expcl2lemap  10781  expclzaplem  10793  expge0  10805  expge1  10806  zsqcl2  10847  bcval4  10982  bcn1  10988  bccl2  10998  hashennnuni  11009  hashunlem  11034  hashdifpr  11050  zfz1isolem1  11070  seq3coll  11072  iswrdiz  11086  ccatsymb  11145  ccatrn  11152  swrds1  11208  swrdccat2  11211  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12lem3  11272  pfxccatin12  11273  pfxccat3  11274  pfxccat3a  11278  shftfn  11343  shftf  11349  recvguniq  11514  resqrexlemdecn  11531  rersqreu  11547  nn0abscl  11604  nnabscl  11619  abs2dif  11625  nn0maxcl  11744  climuni  11812  2clim  11820  climcn2  11828  summodclem2a  11900  fsum3  11906  fsum3cvg3  11915  fsumcl2lem  11917  fsumadd  11925  fisum0diag2  11966  fsummulc2  11967  fsumge0  11978  geolim2  12031  cvgratnnlemabsle  12046  cvgratz  12051  mertenslemi1  12054  prodmodclem3  12094  prodmodclem2a  12095  fprodeq0  12136  fprodge0  12156  eff2  12199  tanvalap  12227  zdvdsdc  12331  fzo0dvdseq  12376  oexpneg  12396  oddge22np1  12400  evennn02n  12401  evennn2n  12402  nno  12425  divalglemeunn  12440  divalglemex  12441  divalglemeuneg  12442  divalg  12443  bitsfzolem  12473  bitsinv1lem  12480  divgcdz  12500  bezoutlemmain  12527  bezoutlemmo  12535  bezoutlemeu  12536  bezoutlemle  12537  sqgcd  12558  uzwodc  12566  nninfctlemfo  12569  eucalgval2  12583  eucalglt  12587  lcmneg  12604  lcmgcdlem  12607  ncoprmgcdne1b  12619  prmind2  12650  prmdc  12660  sqnprm  12666  isprm5lem  12671  isprm5  12672  isprm6  12677  sqrt2irrlem  12691  pw2dvdseu  12698  sqpweven  12705  2sqpwodd  12706  sqrt2irrap  12710  qgt0numnn  12729  phicl2  12744  hashdvds  12751  crth  12754  phimullem  12755  eulerthlem1  12757  eulerthlemh  12761  eulerthlemth  12762  hashgcdlem  12768  oddprm  12790  pythagtriplem6  12801  pythagtriplem11  12805  pythagtriplem13  12807  pythagtriplem19  12813  pclem0  12817  pcpremul  12824  pceu  12826  pc2dvds  12861  difsqpwdvds  12869  pcadd  12871  pockthlem  12887  pockthg  12888  1arith  12898  4sqlemffi  12927  4sqlem11  12932  4sqlem12  12933  4sqlem13m  12934  4sqlem14  12935  4sqlem17  12938  oddennn  12971  evenennn  12972  ennnfoneleminc  12990  ennnfonelemf1  12997  ennnfonelemen  13000  exmidunben  13005  ctinf  13009  ctiunctlemfo  13018  nninfdclemlt  13030  nninfdclemf1  13031  ptex  13305  imasaddfnlemg  13355  imasaddflemg  13357  mgmsscl  13402  sgrp0  13451  sgrp1  13452  hashfinmndnn  13473  ismndd  13478  mndpfo  13479  mhmf1o  13511  0mhm  13527  resmhm  13528  resmhm2  13529  resmhm2b  13530  mhmco  13531  gsumvallem2  13534  isgrpd2e  13561  grpinvf1o  13611  grpinvnzcl  13613  dfgrp3m  13640  mhmmnd  13661  ghmgrp  13663  mulgval  13667  mulgfng  13669  subgmulg  13733  issubg4m  13738  isnsg3  13752  nmzsubg  13755  ssnmz  13756  0nsg  13759  nsgid  13760  ghmnsgima  13813  ghmnsgpreima  13814  ghmf1  13818  kerf1ghm  13819  ghmf1o  13820  conjnmzb  13825  isabld  13844  ghmcmn  13872  ghmabl  13873  invghm  13874  srgfcl  13944  srglmhm  13964  srgrmhm  13965  iscrngd  14013  ringsrg  14018  unitabl  14089  rhmf1o  14140  rhmco  14146  ringelnzr  14159  subrngringnsg  14177  subrgcrng  14197  subrgnzr  14214  resrhm  14220  unitrrg  14239  lssneln0  14346  rnglidlmsgrp  14469  quscrng  14505  expghmap  14579  mulgghm2  14580  znf1o  14623  znidom  14629  znidomb  14630  psrbaglesuppg  14644  tgtopon  14748  distopon  14769  epttop  14772  resttopon  14853  resttopon2  14860  cnco  14903  lmss  14928  txtopon  14944  uptx  14956  txdis1cn  14960  hmeocnv  14989  hmeof1o2  14990  hmeores  14997  hmeoco  14998  idhmeo  14999  txhmeo  15001  txswaphmeo  15003  psmetxrge0  15014  isxmet2d  15030  metres2  15063  xmetresbl  15122  comet  15181  bdxmet  15183  bdmet  15184  tgioo  15236  mulc1cncf  15271  mulcncflem  15289  cnrehmeocntop  15292  cnopnap  15293  dedekindeu  15305  dedekindicclemicc  15314  ivthinclemlm  15316  ivthinclemum  15317  ivthinclemlopn  15318  ivthinclemlr  15319  ivthinclemuopn  15320  ivthinclemur  15321  ivthinclemloc  15323  ivthinc  15325  ivthreinc  15327  dvfgg  15370  dvcjbr  15390  dvcj  15391  dvfre  15392  elplyr  15422  plyreres  15446  rplogbval  15627  sgmnncl  15670  mpodvdsmulf1o  15672  mersenne  15679  perfectlem2  15682  lgsfcl2  15693  lgsval2lem  15697  lgsmod  15713  lgsdirprm  15721  lgsne0  15725  gausslemma2dlem0h  15743  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  gausslemma2dlem4  15751  lgseisenlem1  15757  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem2  15769  2sqlem8  15810  2sqlem9  15811  structiedg0val  15849  ausgrumgrien  15976  usgredgreu  16022  uspgredg2vtxeu  16024  uspgredg2v  16027  usgredg2v  16030  trlres  16108  bj-charfundcALT  16196  bj-nnord  16345  bj-inf2vnlem1  16357  pwf1oexmid  16394  nnsf  16401  nninfall  16405  nninfself  16409  exmidsbthrlem  16420  qdencn  16425