Theorem expr 375

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 365	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 124	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  animpimp2impd  559  reximddv  2580  rexlimdvaa  2595  issod  4318  ordsuc  4561  fcof1  5781  riota5f  5852  ovmpodf  6003  tfrlemi1  6330  eqsuptid  6993  eqinftid  7017  ordiso2  7031  addnq0mo  7443  mulnq0mo  7444  genprndl  7517  genprndu  7518  addlocpr  7532  ltexprlemm  7596  ltexprlemopl  7597  ltexprlemopu  7599  ltexprlemfl  7605  ltexprlemfu  7607  aptiprleml  7635  caucvgprprlemexbt  7702  addsrmo  7739  mulsrmo  7740  prodge0  8807  un0addcl  9205  un0mulcl  9206  seq3fveq2  10464  seq3shft2  10468  monoord  10471  seq3split  10474  seq3id2  10504  expnegzap  10549  expcanlem  10688  bcval5  10736  seq3coll  10815  caucvgrelemcau  10982  cau3lem  11116  reccn2ap  11314  summodclem2  11383  zsumdc  11385  fsumf1o  11391  fisumss  11393  fsumcl2lem  11399  fsumadd  11407  fisum0diag2  11448  fsummulc2  11449  mertenslem2  11537  prodmodclem2  11578  zproddc  11580  fprodseq  11584  fprodf1o  11589  prodssdc  11590  fprodssdc  11591  fprodmul  11592  dvds0lem  11801  dvdsnegb  11808  dvdssub2  11835  isprm6  12139  hashgcdeq  12231  modprminv  12241  modprminveq  12242  reumodprminv  12245  pcqmul  12295  pcqcl  12298  pcxnn0cl  12302  pcxcl  12303  pc2dvds  12321  pcadd  12331  pcmpt  12333  pockthg  12347  infpnlem1  12349  mgmidsssn0  12735  mhmeql  12808  grprcan  12842  dfgrp3mlem  12900  mulgnn0ass  12950  isnsg3  12998  topssnei  13533  innei  13534  cnptopco  13593  cncnpi  13599  cncnp  13601  cnconst2  13604  cnpdis  13613  lmtopcnp  13621  tx2cn  13641  txdis  13648  blssps  13798  blss  13799  neibl  13862  metss  13865  metequiv2  13867  metrest  13877  metcnp3  13882  ivthinclemlopn  13985  ivthinclemlr  13986  ivthinclemuopn  13987  ivthinclemur  13988  ivthinclemloc  13990  2sqlem5  14326  2sqlem6  14327  2sqlem8  14330  2sqlem10  14332  nconstwlpolem  14672