Theorem impl 620

Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)

Hypothesis

Ref	Expression
impl.1

Assertion

Ref	Expression
impl

Proof of Theorem impl

Step	Hyp	Ref	Expression
1		impl.1	. . 3
2	1	expd 436	. 2
3	2	imp31 432	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  sbc2iedv  3404  csbie2t  3463  ordelord  4905  frinxp  5070  foco2  6051  frxp  6910  mpt2curryd  7017  omsmolem  7321  erth  7375  unblem1  7792  unwdomg  8031  cflim2  8664  distrlem1pr  9424  uz11  11132  xmulge0  11505  max0add  13143  prmpwdvds  14422  imasleval  14938  resscntz  16369  ablfac1c  17122  lbsind  17726  mplcoe5lem  18130  cply1mul  18335  isphld  18689  smadiadetr  19177  chfacfisf  19355  chfacfisfcpmat  19356  chcoeffeq  19387  cayhamlem3  19388  tx1stc  20151  ioorcl  21986  coemullem  22647  xrlimcnp  23298  fsumdvdscom  23461  fsumvma  23488  clwlkisclwwlklem2a  24785  clwwlkext2edg  24802  frg2wot1  25057  grpoidinvlem3  25208  htthlem  25834  atcvat4i  27316  abfmpeld  27492  isarchi3  27731  ordtconlem1  27906  funpartfun  29593  ltflcei  30043  neificl  30246  keridl  30429  mpaaeu  31099  lmod0rng  32674  lincext1  33055  cvrat4  35167  ps-2  35202

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