Theorem biadan2 642

Description: Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)

Hypotheses

Ref	Expression
biadan2.1
biadan2.2

Assertion

Ref	Expression
biadan2

Proof of Theorem biadan2

Step	Hyp	Ref	Expression
1		biadan2.1	. . 3
2	1	pm4.71ri 633	. 2
3		biadan2.2	. . 3
4	3	pm5.32i 637	. 2
5	2, 4	bitri 249	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  elab4g  3250  brab2a  5054  brab2ga  5080  elovmpt2  6520  eqop2  6841  iscard  8377  iscard2  8378  elnnnn0  10864  elfzo2  11832  bitsval  14074  1nprm  14222  funcpropd  15269  isfull  15279  isfth  15283  ismhm  15968  isghm  16267  ghmpropd  16304  isga  16329  oppgcntz  16399  gexdvdsi  16603  isrhm  17370  abvpropd  17491  islmhm  17673  dfprm2  18524  prmirred  18525  dfprm2OLD  18527  prmirredOLD  18528  elocv  18699  isobs  18751  iscn2  19739  iscnp2  19740  islocfin  20018  elflim2  20465  isfcls  20510  isnghm  21230  isnmhm  21253  0plef  22079  elply  22592  dchrelbas4  23518  nb3grapr  24453  isph  25737  abfmpunirn  27490  iscvm  28704  sscoid  29563  eldiophb  30690  eldioph3b  30698  eldioph4b  30745  issdrg  31146  ismgmhm  32471  isrnghm  32698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371