Theorem expr 372

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 362	. 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  548  reximddv  2535  rexlimdvaa  2550  issod  4241  ordsuc  4478  fcof1  5684  riota5f  5754  ovmpodf  5902  tfrlemi1  6229  eqsuptid  6884  eqinftid  6908  ordiso2  6920  addnq0mo  7255  mulnq0mo  7256  genprndl  7329  genprndu  7330  addlocpr  7344  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemfl  7417  ltexprlemfu  7419  aptiprleml  7447  caucvgprprlemexbt  7514  addsrmo  7551  mulsrmo  7552  prodge0  8612  un0addcl  9010  un0mulcl  9011  seq3fveq2  10242  seq3shft2  10246  monoord  10249  seq3split  10252  seq3id2  10282  expnegzap  10327  expcanlem  10462  bcval5  10509  seq3coll  10585  caucvgrelemcau  10752  cau3lem  10886  reccn2ap  11082  summodclem2  11151  zsumdc  11153  fsumf1o  11159  fisumss  11161  fsumcl2lem  11167  fsumadd  11175  fisum0diag2  11216  fsummulc2  11217  mertenslem2  11305  prodmodclem2  11346  dvds0lem  11503  dvdsnegb  11510  dvdssub2  11535  isprm6  11825  hashgcdeq  11904  topssnei  12331  innei  12332  cnptopco  12391  cncnpi  12397  cncnp  12399  cnconst2  12402  cnpdis  12411  lmtopcnp  12419  tx2cn  12439  txdis  12446  blssps  12596  blss  12597  neibl  12660  metss  12663  metequiv2  12665  metrest  12675  metcnp3  12680  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788