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  554  reximddv  2573  rexlimdvaa  2588  issod  4304  ordsuc  4547  fcof1  5762  riota5f  5833  ovmpodf  5984  tfrlemi1  6311  eqsuptid  6974  eqinftid  6998  ordiso2  7012  addnq0mo  7409  mulnq0mo  7410  genprndl  7483  genprndu  7484  addlocpr  7498  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemfl  7571  ltexprlemfu  7573  aptiprleml  7601  caucvgprprlemexbt  7668  addsrmo  7705  mulsrmo  7706  prodge0  8770  un0addcl  9168  un0mulcl  9169  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  seq3id2  10465  expnegzap  10510  expcanlem  10649  bcval5  10697  seq3coll  10777  caucvgrelemcau  10944  cau3lem  11078  reccn2ap  11276  summodclem2  11345  zsumdc  11347  fsumf1o  11353  fisumss  11355  fsumcl2lem  11361  fsumadd  11369  fisum0diag2  11410  fsummulc2  11411  mertenslem2  11499  prodmodclem2  11540  zproddc  11542  fprodseq  11546  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodmul  11554  dvds0lem  11763  dvdsnegb  11770  dvdssub2  11797  isprm6  12101  hashgcdeq  12193  modprminv  12203  modprminveq  12204  reumodprminv  12207  pcqmul  12257  pcqcl  12260  pcxnn0cl  12264  pcxcl  12265  pc2dvds  12283  pcadd  12293  pcmpt  12295  pockthg  12309  infpnlem1  12311  mgmidsssn0  12638  mhmeql  12707  grprcan  12740  topssnei  12956  innei  12957  cnptopco  13016  cncnpi  13022  cncnp  13024  cnconst2  13027  cnpdis  13036  lmtopcnp  13044  tx2cn  13064  txdis  13071  blssps  13221  blss  13222  neibl  13285  metss  13288  metequiv2  13290  metrest  13300  metcnp3  13305  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  2sqlem5  13749  2sqlem6  13750  2sqlem8  13753  2sqlem10  13755  nconstwlpolem  14096