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  4319  ordsuc  4562  fcof1  5783  riota5f  5854  ovmpodf  6005  tfrlemi1  6332  eqsuptid  6995  eqinftid  7019  ordiso2  7033  addnq0mo  7445  mulnq0mo  7446  genprndl  7519  genprndu  7520  addlocpr  7534  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemfl  7607  ltexprlemfu  7609  aptiprleml  7637  caucvgprprlemexbt  7704  addsrmo  7741  mulsrmo  7742  prodge0  8810  un0addcl  9208  un0mulcl  9209  seq3fveq2  10468  seq3shft2  10472  monoord  10475  seq3split  10478  seq3id2  10508  expnegzap  10553  expcanlem  10694  bcval5  10742  seq3coll  10821  caucvgrelemcau  10988  cau3lem  11122  reccn2ap  11320  summodclem2  11389  zsumdc  11391  fsumf1o  11397  fisumss  11399  fsumcl2lem  11405  fsumadd  11413  fisum0diag2  11454  fsummulc2  11455  mertenslem2  11543  prodmodclem2  11584  zproddc  11586  fprodseq  11590  fprodf1o  11595  prodssdc  11596  fprodssdc  11597  fprodmul  11598  dvds0lem  11807  dvdsnegb  11814  dvdssub2  11841  isprm6  12146  hashgcdeq  12238  modprminv  12248  modprminveq  12249  reumodprminv  12252  pcqmul  12302  pcqcl  12305  pcxnn0cl  12309  pcxcl  12310  pc2dvds  12328  pcadd  12338  pcmpt  12340  pockthg  12354  infpnlem1  12356  mgmidsssn0  12802  mhmeql  12875  grprcan  12909  dfgrp3mlem  12967  mulgnn0ass  13017  isnsg3  13065  topssnei  13632  innei  13633  cnptopco  13692  cncnpi  13698  cncnp  13700  cnconst2  13703  cnpdis  13712  lmtopcnp  13720  tx2cn  13740  txdis  13747  blssps  13897  blss  13898  neibl  13961  metss  13964  metequiv2  13966  metrest  13976  metcnp3  13981  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemloc  14089  2sqlem5  14436  2sqlem6  14437  2sqlem8  14440  2sqlem10  14442  nconstwlpolem  14782