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  4317  ordsuc  4560  fcof1  5779  riota5f  5850  ovmpodf  6001  tfrlemi1  6328  eqsuptid  6991  eqinftid  7015  ordiso2  7029  addnq0mo  7441  mulnq0mo  7442  genprndl  7515  genprndu  7516  addlocpr  7530  ltexprlemm  7594  ltexprlemopl  7595  ltexprlemopu  7597  ltexprlemfl  7603  ltexprlemfu  7605  aptiprleml  7633  caucvgprprlemexbt  7700  addsrmo  7737  mulsrmo  7738  prodge0  8805  un0addcl  9203  un0mulcl  9204  seq3fveq2  10462  seq3shft2  10466  monoord  10469  seq3split  10472  seq3id2  10502  expnegzap  10547  expcanlem  10686  bcval5  10734  seq3coll  10813  caucvgrelemcau  10980  cau3lem  11114  reccn2ap  11312  summodclem2  11381  zsumdc  11383  fsumf1o  11389  fisumss  11391  fsumcl2lem  11397  fsumadd  11405  fisum0diag2  11446  fsummulc2  11447  mertenslem2  11535  prodmodclem2  11576  zproddc  11578  fprodseq  11582  fprodf1o  11587  prodssdc  11588  fprodssdc  11589  fprodmul  11590  dvds0lem  11799  dvdsnegb  11806  dvdssub2  11833  isprm6  12137  hashgcdeq  12229  modprminv  12239  modprminveq  12240  reumodprminv  12243  pcqmul  12293  pcqcl  12296  pcxnn0cl  12300  pcxcl  12301  pc2dvds  12319  pcadd  12329  pcmpt  12331  pockthg  12345  infpnlem1  12347  mgmidsssn0  12733  mhmeql  12804  grprcan  12838  dfgrp3mlem  12896  mulgnn0ass  12946  topssnei  13444  innei  13445  cnptopco  13504  cncnpi  13510  cncnp  13512  cnconst2  13515  cnpdis  13524  lmtopcnp  13532  tx2cn  13552  txdis  13559  blssps  13709  blss  13710  neibl  13773  metss  13776  metequiv2  13778  metrest  13788  metcnp3  13793  ivthinclemlopn  13896  ivthinclemlr  13897  ivthinclemuopn  13898  ivthinclemur  13899  ivthinclemloc  13901  2sqlem5  14237  2sqlem6  14238  2sqlem8  14241  2sqlem10  14243  nconstwlpolem  14583