Theorem 3impia 828

Description: Importation to triple conjunction.

Hypothesis

Ref	Expression
3impia.1	|- ((ph /\ ps) -> (ch -> th))

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 |- ((ph /\ ps) -> (ch -> th))
2	1	ex 373	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 825	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773

This theorem is referenced by:  3gencl 1821  vtoclegft 1847  disjne 2305  opthgg 2779  tz7.2 2921  ndmoprg 4028  oaass 4179  xpdom1g 4424  unidomg 4781  axsup 5479  ltnet 5488  xrltnet 5538  divclt 5681  divcan1t 5689  divcan2t 5690  divrect 5702  divcan3t 5718  redivclt 5756  letrp1t 5772  p1let 5773  zextlet 6136  zextltt 6137  btwnnzt 6139  gtndivt 6140  uzind2 6154  flwordit 6183  ceilet 6193  qbtwnre 6216  qbtwnxr 6217  snunioo 6348  elfz4t 6407  expge1t 6524  exple1t 6538  absdivt 6795  cjdivt 6827  bccl2t 6909  fsum1ps 6956  iserzext 7071  isumreclt 7145  cncffvelrnOLD 7202  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  znnenlem 7443  clsndisj 7648  metcni 7833  lmfss 7883  lmcl 7884  bcthlem8 7940  bcth 7966  grpasscan1OLD 8008  grpasscan1 8012  grplactf1o 8034  nvs 8229  nvtri 8237  nmlno0 8387  nmlnoubi 8388  hlipgt0 8546  sincosq1lem 8620  efifolem4 8640  efifolem5 8641  ocnelt 9086  elspansn2t 9406  elspansn3t 9412  normcant 9416  pjoml2t 9471  lecmt 9477  osumt 9505  nmbdfnlbt 9894  leopmult 9979  hstpytht 10066  cvnbtwnt 10123  ssmd1 10146  ssmd2 10147  ssdmd1 10148  ssdmd2 10149  cvmdt 10171  cvdmdt 10172  superpos 10189  cayleylem2 10317  cnvhmphb 10413  dmse1 10467  mslb1 10473  2wsms 10474  cmpassoh 10573  cmpmon 10585  icmpmon 10587

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  df-3an 775

Copyright terms: Public domain