Theorem imp32 361

Description: An importation inference.

Hypothesis

Ref	Expression
imp3.1	⊢ (φ → (ψ → (χ → θ)))

Assertion

Ref	Expression
imp32	⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)

Proof of Theorem imp32

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 ⊢ (φ → (ψ → (χ → θ)))
2	1	imp3a 359	. 2 ⊢ (φ → ((ψ ⋀ χ) → θ))
3	2	imp 348	1 ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  imp42 367  anasss 442  ancom2s 490  ancom13s 491  3expb 840  reuss2 2327  reupick 2331  po2nr 2925  tz7.7 3001  onint 3152  isomin 4013  tfrlem5 4216  tz7.48lem 4256  oalimcl 4330  oaass 4331  omass 4347  oelim2 4358  en3d 4542  zorn2lem7 4940  addclpi 5174  addnidpi 5182  genpnnp 5262  genpnmax 5264  mulclprlem 5275  prlem936b 5308  lemul1aOLD 5982  peano2uz2 6372  uzwo3lem1 6388  uzwo3lem2 6389  elfz4 6603  fsequb 6654  expwordi 6800  sqrlem6 6879  replim 6962  seq1ublem 7114  bccl2 7174  fsumcllem 7217  2climnn 7305  2climnn0 7306  climcmpc1 7342  isummulc1 7416  cvgratlem1ALT 7452  cvgratlem4 7458  infpnlem1 7718  tgss2 7849  0ntr 7912  clsndisj 7916  neindisj 7941  innei 7946  islpi 7959  cnsscnp 7982  cncnpi 7983  cnconst 7990  opni2 8075  lmcvg 8143  lmnn 8146  metcnp4lem2 8180  metcn4i 8183  bcthlem21 8230  grpidinvlem3 8263  ubthlem13 8800  ubthlem13OLD 8801  spansncol 9767  elspansn5 9773  5oalem6 9882  lnopconi 10242  lnfnconi 10269  nlelchi 10273  leopmul2i 10348  mdi 10503  dmdi 10510  dmdsl3 10523  atom1d 10561  cvexchlem 10576  atcvatlem 10594  irredlem3 10601  mdsymlem5 10616  cdj1i 10642  nndivsub 10706  hmeogrp 11044  ltsubpostb 11150  ltaddpos2tb 11151  idmon 11272  impr 11359  elicc3 11410  finsschain 11425  cnntr 11474  comptoppr 11495  conntoppr 11504  reconnlem1 11507  fnemeet1 11589  fnemeet2 11590  isufil2 11650  filssufillem 11655  filufint 11659  ufilen 11664  fcluscnplem 11729  haustlmu 11967  rrncms 12075  phtpcer 12104

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

Copyright terms: Public domain