Theorem sylanbrc 411

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 302	. 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sb2  1708  sbequ1  1709  sbidm  1790  eqeu  2807  euind  2824  reuind  2842  eldifd  3031  eqssd  3064  ssrabdv  3123  elind  3208  dcun  3420  opm  4094  issod  4179  ordsucim  4354  onintonm  4371  ordtri2or2exmidlem  4379  en2lp  4407  ordwe  4428  sosng  4550  sotri2  4872  sotri3  4873  relssdmrn  4995  funun  5103  fnsng  5106  fnprg  5114  fntpg  5115  fntp  5116  fununi  5127  imain  5141  fnco  5167  f00  5250  f1ss  5270  f1ssr  5271  f1ssres  5273  f1f1orn  5312  foimacnv  5319  foun  5320  fun11iun  5322  sefvex  5374  dff3im  5497  fmpt  5502  ffnfv  5510  fmpt2d  5514  ffvresb  5515  fprg  5535  foco2  5587  fcof1  5616  fcofo  5617  fcof1o  5622  fliftf  5632  isoini2  5652  f1oiso  5659  moriotass  5690  fnoprabg  5804  f1ocnvd  5904  suppssfv  5910  suppssov1  5911  1stcof  5992  2ndcof  5993  1stconst  6048  2ndconst  6049  fo2ndf  6054  f1o2ndf1  6055  f1od2  6062  smores2  6121  tfrlem5  6141  tfrlemibfn  6155  tfr1onlembfn  6171  tfri1dALT  6178  tfrcllembfn  6184  nntri2  6320  eroveu  6450  elixpsn  6559  dom2lem  6596  xpf1o  6667  fidifsnen  6693  finexdc  6725  unfidisj  6739  f1finf1o  6763  fidcenumlemrks  6769  sbthlemi9  6781  supeuti  6796  infeuti  6831  casef1  6890  caseinl  6891  caseinr  6892  difinfsnlem  6899  ctmlemr  6908  ctm  6909  ctssdclemn0  6910  ctssdclemr  6911  ctssdc  6912  enumctlemm  6913  nnnninf  6935  en2other2  6961  exmidfodomrlemim  6966  addclpi  7036  mulclpi  7037  nnppipi  7052  recmulnqg  7100  enq0ref  7142  nqnq0pi  7147  genipv  7218  addclpr  7246  nqprxx  7255  prmuloc  7275  mulclpr  7281  distrlem1prl  7291  distrlem1pru  7292  ltexprlempr  7317  ltexprlemrl  7319  ltexprlemru  7321  lteupri  7326  recexprlempr  7341  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemlol  7356  cauappcvgprlemopu  7357  cauappcvgprlemupu  7358  cauappcvgprlemloc  7361  cauappcvgprlemcl  7362  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  cauappcvgprlem2  7369  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemlol  7379  caucvgprlemopu  7380  caucvgprlemupu  7381  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlem2  7389  caucvgprprlemml  7403  caucvgprprlemmu  7404  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemupu  7409  caucvgprprlemloc  7412  caucvgprprlemcl  7413  caucvgprprlem2  7419  elrealeu  7517  rereceu  7574  negf1o  8011  receuap  8291  divvalap  8295  cju  8577  nn0ge2m1nn  8889  nnnegz  8909  elnnz  8916  elnn0z  8919  peano2z  8942  nn0n0n1ge2  8973  msqznn  9003  eluzaddi  9202  eluzsubi  9203  uzind4  9233  supinfneg  9240  infsupneg  9241  elnn1uz2  9251  uz2mulcl  9252  divfnzn  9263  nnrp  9300  rpaddcl  9314  rpmulcl  9315  rpdivcl  9316  rpgecl  9319  ge0p1rp  9322  elrpd  9328  ge0addcl  9605  ge0mulcl  9606  ge0xaddcl  9607  icoshftf1o  9615  peano2fzr  9658  uzsubsubfz  9668  fzsplit2  9671  elfznn  9675  fzss1  9684  fzss2  9685  fzp1elp1  9696  elfz1b  9711  elfz0fzfz0  9744  fz0fzelfz0  9745  difelfznle  9753  elfzofz  9780  fzosplitsnm1  9827  ubmelm1fzo  9844  fzofzp1b  9846  fzosplitsn  9851  exbtwnz  9869  flqge0nn0  9907  flqge1nn  9908  zmodcl  9958  modqmuladdnn0  9982  modsumfzodifsn  10010  frec2uzf1od  10020  frec2uzisod  10021  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgtcl  10026  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgfunlem  10033  frecuzrdgtclt  10035  frecuzrdgsuctlem  10037  uzennn  10050  seq3fveq2  10083  monoord  10090  iseqf1olemqcl  10100  iseqf1olemnab  10102  iseqf1olemab  10103  iseqf1olemqf1o  10107  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3id2  10123  exp3val  10136  expcl2lemap  10146  expclzaplem  10158  expge0  10170  expge1  10171  zsqcl2  10211  bcval4  10339  bcn1  10345  bccl2  10355  hashennnuni  10366  hashunlem  10391  hashdifpr  10407  zfz1isolem1  10424  seq3coll  10426  shftfn  10437  shftf  10443  recvguniq  10607  resqrexlemdecn  10624  rersqreu  10640  nn0abscl  10697  nnabscl  10712  abs2dif  10718  climuni  10901  2clim  10909  climcn2  10917  summodclem2a  10989  fsum3  10995  fsum3cvg3  11004  fsumcl2lem  11006  fsumadd  11014  fisum0diag2  11055  fsummulc2  11056  fsumge0  11067  geolim2  11120  cvgratnnlemabsle  11135  cvgratz  11140  mertenslemi1  11143  eff2  11184  tanvalap  11213  zdvdsdc  11309  fzo0dvdseq  11350  oexpneg  11369  oddge22np1  11373  evennn02n  11374  evennn2n  11375  nno  11398  divalglemeunn  11413  divalglemex  11414  divalglemeuneg  11415  divalg  11416  zsupcllemstep  11433  zsupcl  11435  divgcdz  11455  bezoutlemmain  11479  bezoutlemmo  11487  bezoutlemeu  11488  bezoutlemle  11489  sqgcd  11510  eucalgval2  11527  eucalglt  11531  lcmcllem  11541  lcmledvds  11544  lcmneg  11548  lcmgcdlem  11551  ncoprmgcdne1b  11563  prmind2  11594  sqnprm  11609  isprm6  11618  sqrt2irrlem  11632  pw2dvdseu  11638  sqpweven  11645  2sqpwodd  11646  sqrt2irrap  11650  qgt0numnn  11669  phicl2  11682  hashdvds  11689  crth  11692  phimullem  11693  hashgcdlem  11695  oddennn  11697  evenennn  11698  ennnfoneleminc  11716  ennnfonelemf1  11723  ennnfonelemen  11726  exmidunben  11731  ctinf  11735  tgtopon  12017  distopon  12038  epttop  12041  resttopon  12122  resttopon2  12129  cnco  12171  lmss  12196  txtopon  12212  uptx  12224  txdis1cn  12228  psmetxrge0  12260  isxmet2d  12276  metres2  12309  xmetresbl  12368  comet  12427  bdxmet  12429  bdmet  12430  tgioo  12465  mulc1cncf  12489  mulcncflem  12502  dvfgg  12530  bj-nnord  12741  bj-inf2vnlem1  12753  pwf1oexmid  12780  nnsf  12783  nninfall  12788  nninfself  12793  exmidsbthrlem  12801  qdencn  12806