Theorem 3impia 836

Description: Importation to triple conjunction.

Hypothesis

Ref	Expression
3impia.1	⊢ ((φ ⋀ ψ) → (χ → θ))

Assertion

Ref	Expression
3impia	⊢ ((φ ⋀ ψ ⋀ χ) → θ)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((φ ⋀ ψ) → (χ → θ))
2	1	ex 371	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	3imp 833	1 ⊢ ((φ ⋀ ψ ⋀ χ) → θ)

Syntax hints:   → wi 3   ⋀ wa 221   ⋀ w3a 781

This theorem is referenced by:  3gencl 1876  vtoclegft 1902  disjne 2368  opthgg 2865  tz7.2 2959  ndmoprg 4104  oaass 4331  oeoalem 4359  oeoelem 4361  xpdom1g 4585  unidomg 4955  cdaung 5073  cdaeng 5076  axsup 5661  ltne 5670  xrltne 5719  divcl 5864  divcan1 5872  divrec 5885  divcan3 5901  redivcl 5940  letrp1 5956  p1le 5957  zextle 6360  zextlt 6361  btwnnz 6363  gtndiv 6364  uzind2 6377  qbtwnre 6418  qbtwnxr 6419  flwordi 6436  ceile 6450  modadd1 6477  modmul1 6478  modirr 6481  snunioo 6542  elfz4 6603  expge1 6787  exprec 6789  exple1 6804  absdiv 7062  cjdiv 7092  bccl2 7174  fsum1ps 7221  iserzex 7338  isumrecl 7414  explecnv 7438  cncffvelrnOLD 7472  ivthlem6 7491  ivthlem7 7492  znnenlem 7713  clsndisj 7916  metcni 8105  lmfss 8159  lmcl 8160  bcthlem8 8217  bcth 8243  grpasscan1 8294  gxnn0neg 8319  gxnn0suc 8320  gxcl 8321  gxneg 8322  gxcom 8325  gxinv 8326  gxsuc 8328  gxnn0add 8330  gxadd 8331  gxnn0mul 8333  gxmul 8334  grplactf1o 8339  gxdi 8355  nvs 8537  nvtri 8545  nmlno0 8710  nmlnoubi 8711  hlipgt0 8878  spwnex 8923  sincosq1lem 8970  efifolem4 8997  efifolem5 8998  ocnel 9446  elspansn2 9766  elspansn3 9771  normcan 9775  pjoml2 9830  lecm 9836  osum 9866  nmbdfnlb 10258  leopmul 10347  hstpyth 10437  cvnbtwn 10494  ssmd1 10519  ssmd2 10520  ssdmd1 10521  ssdmd2 10522  cvmd 10544  cvdmd 10545  superpos 10562  cayleylem2 10695  sfseqeq 10824  jop 10832  mop 10833  labs1 10836  labs2 10838  cnvhmphb 11032  bwt2 11123  dmse1 11146  mslb1 11152  2wsms 11153  cmpassoh 11256  cmpmon 11270  icmpmon 11271  iccleub 11411  hausnei2 11471  hmeoclda 11475  hmeocldb 11476  compcov 11486  hscptsscld 11491  compfipin0lem 11492  comptoppr 11495  alexsub 11500  conntoppr 11504  fnessex 11545  fneuni 11546  refssex 11551  locfinnei 11573  fbssint 11626  ufilen 11664  flimnei 11678  limfilss 11682  fclusneii 11721  fclsfnflim 11726  gagrpid 11780  gaass 11781  erthdmg 11824  dif1en 11833  fipreima 11848  inficl 11849  eluzsub 11861  incsequz 11879  iserzshft2 11892  subspcld2 11902  iccsplit 11919  iimulcl 11938  paste 11954  ismtybndlem 12008  ismtybnd 12009  heiborlem13 12023  bfp 12065

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 145  df-an 223  df-3an 783

Copyright terms: Public domain