Theorem imp32 363

Description: An importation inference.

Hypothesis

Ref	Expression
imp3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
imp32	|- ((ph /\ (ps /\ ch)) -> th)

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 |- (ph -> (ps -> (ch -> th)))
2	1	imp3a 361	. 2 |- (ph -> ((ps /\ ch) -> th))
3	2	imp 350	1 |- ((ph /\ (ps /\ ch)) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imp42 369  anasss 440  ancom2s 487  ancom13s 488  3expb 834  reuss2 2275  reupick 2279  po2nr 2847  tz7.7 2973  onint 3006  isomin 3899  tfrlem5 3915  tz7.48lem 3955  oalimcl 4194  oaass 4195  omass 4211  oelim2 4222  en3d 4401  zorn2lem7 4794  addclpi 5020  addnidpi 5028  genpnnp 5108  genpnmax 5110  mulclprlem 5121  prlem936b 5154  lemul1itOLD 5838  peano2uz2 6201  uzwo3lem1 6216  uzwo3lem2 6217  elfz4t 6475  fsequb 6523  expwordit 6603  sqrlem6 6678  replimt 6761  seq1ublem 6911  bccl2t 6971  fsumcllem 7014  2climnn 7102  2climnn0 7103  climcmpc1 7139  isummulc1 7212  cvgratlem1ALT 7247  cvgratlem4 7253  infpnlem1 7506  tgss2t 7637  0ntr 7702  clsndisj 7706  neindisj 7731  innei 7736  islpi 7749  cnsscnp 7772  cncnpi 7773  cnconst 7780  opni2 7865  lmcvg 7932  lmnn 7935  metcnp4lem2 7969  metcn4i 7972  bcthlem21 8019  grpidinvlem3 8050  ubthlem13 8541  spansncol 9491  elspansn5t 9497  5oalem6 9604  lnopcon 9963  lnfncon 9990  nlelch 9994  leopmul2it 10068  mdit 10222  dmdit 10229  dmdsl3t 10242  atom1d 10280  cvexchlem 10295  atcvatlem 10312  irredlem3 10319  mdsymlem5 10334  cdj1 10360  nndivsub 10421  hmeogrp 10538  ltsubpostb 10627  ltaddpos2tb 10628  idmon 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain