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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  animpimp2impd  565  reximddv  2653  rexlimdvaa  2669  issod  4464  ordsuc  4710  fcof1  5989  riota5f  6065  ovmpodf  6220  suppssdc  6500  tfrlemi1  6603  eqsuptid  7337  eqinftid  7361  ordiso2  7375  addnq0mo  7814  mulnq0mo  7815  genprndl  7888  genprndu  7889  addlocpr  7903  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemfu  7978  aptiprleml  8006  caucvgprprlemexbt  8073  addsrmo  8110  mulsrmo  8111  prodge0  9185  un0addcl  9598  un0mulcl  9599  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  monoord  10924  seq3split  10927  seqsplitg  10928  seqf1oglem1  10958  seq3id2  10965  seqhomog  10969  expnegzap  11012  expcanlem  11155  bcval5  11203  hashfibc  11285  seq3coll  11296  wrdind  11496  wrd2ind  11497  caucvgrelemcau  11748  cau3lem  11882  reccn2ap  12081  summodclem2  12151  zsumdc  12153  fsumf1o  12159  fisumss  12161  fsumcl2lem  12167  fsumadd  12175  fisum0diag2  12216  fsummulc2  12217  mertenslem2  12305  prodmodclem2  12346  zproddc  12348  fprodseq  12352  fprodf1o  12357  prodssdc  12358  fprodssdc  12359  fprodmul  12360  dvds0lem  12570  dvdsnegb  12577  dvdssub2  12604  isprm6  12927  hashgcdeq  13020  modprminv  13030  modprminveq  13031  reumodprminv  13034  pcqmul  13084  pcqcl  13087  pcxnn0cl  13091  pcxcl  13092  pc2dvds  13111  pcadd  13121  pcmpt  13124  pockthg  13138  infpnlem1  13140  ballotfilemfc0  13234  ballotfilemfcc  13235  mgmidsssn0  13706  mhmeql  13801  grprcan  13844  dfgrp3mlem  13905  mulgnn0ass  13963  isnsg3  14012  ghmpreima  14071  ghmeql  14072  lss1d  14722  znidomb  14995  rnasclassa  15040  topssnei  15265  innei  15266  cnptopco  15325  cncnpi  15331  cncnp  15333  cnconst2  15336  cnpdis  15345  lmtopcnp  15353  tx2cn  15373  txdis  15380  blssps  15530  blss  15531  neibl  15594  metss  15597  metequiv2  15599  metrest  15609  metcnp3  15614  ivthinclemlopn  15739  ivthinclemlr  15740  ivthinclemuopn  15741  ivthinclemur  15742  ivthinclemloc  15744  plycolemc  15861  mpodvdsmulf1o  16110  perfectlem2  16120  2sqlem5  16250  2sqlem6  16251  2sqlem8  16254  2sqlem10  16256  nconstwlpolem  17127