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  2590  rexlimdvaa  2605  issod  4331  ordsuc  4574  fcof1  5797  riota5f  5868  ovmpodf  6019  tfrlemi1  6346  eqsuptid  7009  eqinftid  7033  ordiso2  7047  addnq0mo  7459  mulnq0mo  7460  genprndl  7533  genprndu  7534  addlocpr  7548  ltexprlemm  7612  ltexprlemopl  7613  ltexprlemopu  7615  ltexprlemfl  7621  ltexprlemfu  7623  aptiprleml  7651  caucvgprprlemexbt  7718  addsrmo  7755  mulsrmo  7756  prodge0  8824  un0addcl  9222  un0mulcl  9223  seq3fveq2  10482  seq3shft2  10486  monoord  10489  seq3split  10492  seq3id2  10522  expnegzap  10567  expcanlem  10708  bcval5  10756  seq3coll  10835  caucvgrelemcau  11002  cau3lem  11136  reccn2ap  11334  summodclem2  11403  zsumdc  11405  fsumf1o  11411  fisumss  11413  fsumcl2lem  11419  fsumadd  11427  fisum0diag2  11468  fsummulc2  11469  mertenslem2  11557  prodmodclem2  11598  zproddc  11600  fprodseq  11604  fprodf1o  11609  prodssdc  11610  fprodssdc  11611  fprodmul  11612  dvds0lem  11821  dvdsnegb  11828  dvdssub2  11855  isprm6  12160  hashgcdeq  12252  modprminv  12262  modprminveq  12263  reumodprminv  12266  pcqmul  12316  pcqcl  12319  pcxnn0cl  12323  pcxcl  12324  pc2dvds  12342  pcadd  12352  pcmpt  12354  pockthg  12368  infpnlem1  12370  mgmidsssn0  12821  mhmeql  12897  grprcan  12933  dfgrp3mlem  12994  mulgnn0ass  13050  isnsg3  13098  lss1d  13567  topssnei  13933  innei  13934  cnptopco  13993  cncnpi  13999  cncnp  14001  cnconst2  14004  cnpdis  14013  lmtopcnp  14021  tx2cn  14041  txdis  14048  blssps  14198  blss  14199  neibl  14262  metss  14265  metequiv2  14267  metrest  14277  metcnp3  14282  ivthinclemlopn  14385  ivthinclemlr  14386  ivthinclemuopn  14387  ivthinclemur  14388  ivthinclemloc  14390  2sqlem5  14737  2sqlem6  14738  2sqlem8  14741  2sqlem10  14743  nconstwlpolem  15085