Theorem expr 373

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
expr.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
expr	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	exp32 363	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 123	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  animpimp2impd  549  reximddv  2538  rexlimdvaa  2553  issod  4249  ordsuc  4486  fcof1  5692  riota5f  5762  ovmpodf  5910  tfrlemi1  6237  eqsuptid  6892  eqinftid  6916  ordiso2  6928  addnq0mo  7279  mulnq0mo  7280  genprndl  7353  genprndu  7354  addlocpr  7368  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemfl  7441  ltexprlemfu  7443  aptiprleml  7471  caucvgprprlemexbt  7538  addsrmo  7575  mulsrmo  7576  prodge0  8636  un0addcl  9034  un0mulcl  9035  seq3fveq2  10273  seq3shft2  10277  monoord  10280  seq3split  10283  seq3id2  10313  expnegzap  10358  expcanlem  10493  bcval5  10541  seq3coll  10617  caucvgrelemcau  10784  cau3lem  10918  reccn2ap  11114  summodclem2  11183  zsumdc  11185  fsumf1o  11191  fisumss  11193  fsumcl2lem  11199  fsumadd  11207  fisum0diag2  11248  fsummulc2  11249  mertenslem2  11337  prodmodclem2  11378  zproddc  11380  fprodseq  11384  dvds0lem  11539  dvdsnegb  11546  dvdssub2  11571  isprm6  11861  hashgcdeq  11940  topssnei  12370  innei  12371  cnptopco  12430  cncnpi  12436  cncnp  12438  cnconst2  12441  cnpdis  12450  lmtopcnp  12458  tx2cn  12478  txdis  12485  blssps  12635  blss  12636  neibl  12699  metss  12702  metequiv2  12704  metrest  12714  metcnp3  12719  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827