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  2568  rexlimdvaa  2583  issod  4296  ordsuc  4539  fcof1  5750  riota5f  5821  ovmpodf  5969  tfrlemi1  6296  eqsuptid  6958  eqinftid  6982  ordiso2  6996  addnq0mo  7384  mulnq0mo  7385  genprndl  7458  genprndu  7459  addlocpr  7473  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemfl  7546  ltexprlemfu  7548  aptiprleml  7576  caucvgprprlemexbt  7643  addsrmo  7680  mulsrmo  7681  prodge0  8745  un0addcl  9143  un0mulcl  9144  seq3fveq2  10400  seq3shft2  10404  monoord  10407  seq3split  10410  seq3id2  10440  expnegzap  10485  expcanlem  10624  bcval5  10672  seq3coll  10751  caucvgrelemcau  10918  cau3lem  11052  reccn2ap  11250  summodclem2  11319  zsumdc  11321  fsumf1o  11327  fisumss  11329  fsumcl2lem  11335  fsumadd  11343  fisum0diag2  11384  fsummulc2  11385  mertenslem2  11473  prodmodclem2  11514  zproddc  11516  fprodseq  11520  fprodf1o  11525  prodssdc  11526  fprodssdc  11527  fprodmul  11528  dvds0lem  11737  dvdsnegb  11744  dvdssub2  11771  isprm6  12075  hashgcdeq  12167  modprminv  12177  modprminveq  12178  reumodprminv  12181  pcqmul  12231  pcqcl  12234  pcxnn0cl  12238  pcxcl  12239  pc2dvds  12257  pcadd  12267  pcmpt  12269  pockthg  12283  infpnlem1  12285  topssnei  12762  innei  12763  cnptopco  12822  cncnpi  12828  cncnp  12830  cnconst2  12833  cnpdis  12842  lmtopcnp  12850  tx2cn  12870  txdis  12877  blssps  13027  blss  13028  neibl  13091  metss  13094  metequiv2  13096  metrest  13106  metcnp3  13111  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  2sqlem5  13555  2sqlem6  13556  2sqlem8  13559  2sqlem10  13561  nconstwlpolem  13903