Theorem impancom 260

Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)

Hypothesis

Ref	Expression
impancom.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
impancom	⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Proof of Theorem impancom

Step	Hyp	Ref	Expression
1		impancom.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 124	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

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:  eqrdav  2228  disjiun  4081  euotd  4345  onsucelsucr  4604  isotr  5952  spc2ed  6393  nninfninc  7313  ltbtwnnqq  7625  genpcdl  7729  genpcuu  7730  un0addcl  9425  un0mulcl  9426  btwnnz  9564  uznfz  10328  elfz0ubfz0  10350  fzoss1  10398  elfzo0z  10413  fzofzim  10417  elfzom1p1elfzo  10449  ssfzo12bi  10460  subfzo0  10478  modfzo0difsn  10647  expaddzap  10835  ccatalpha  11180  swrdswrdlem  11275  swrdswrd  11276  swrdccatin1  11296  pfxccatin12lem3  11303  caucvgre  11532  caubnd2  11668  summodc  11934  fzo0dvdseq  12408  nno  12457  lcmdvds  12641  hashgcdeq  12802  modprm0  12817  pcqcl  12869  issubg4m  13770  01eq0ring  14193  neii1  14861  neii2  14863  fsumcncntop  15281  gausslemma2dlem1a  15777  usgrislfuspgrdom  16029  upgrwlkvtxedg  16161  uspgr2wlkeq  16162  clwwlkccatlem  16195  clwwlknonex2lem2  16233