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 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  eqrdav  2237  disjiun  4125  euotd  4397  onsucelsucr  4657  isotr  6025  spc2ed  6473  nninfninc  7469  ltbtwnnqq  7788  genpcdl  7892  genpcuu  7893  un0addcl  9607  un0mulcl  9608  btwnnz  9751  uznfz  10527  elfz0ubfz0  10549  fzoss1  10597  elfzo0z  10613  fzofzim  10617  elfzom1p1elfzo  10649  ssfzo12bi  10660  subfzo0  10678  modfzo0difsn  10853  expaddzap  11041  ccatalpha  11403  swrdswrdlem  11498  swrdswrd  11499  swrdccatin1  11519  pfxccatin12lem3  11526  caucvgre  11769  caubnd2  11906  summodc  12175  fzo0dvdseq  12649  nno  12698  lcmdvds  12882  hashgcdeq  13047  modprm0  13062  pcqcl  13114  issubg4m  14055  resscntz  14166  01eq0ring  14605  neii1  15373  neii2  15375  fsumcncntop  15793  gausslemma2dlem1a  16382  usgrislfuspgrdom  16636  upgrwlkvtxedg  16810  uspgr2wlkeq  16811  clwwlkccatlem  16846  clwwlknonex2lem2  16884