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  2188  disjiun  4013  euotd  4269  onsucelsucr  4522  isotr  5833  spc2ed  6252  ltbtwnnqq  7432  genpcdl  7536  genpcuu  7537  un0addcl  9227  un0mulcl  9228  btwnnz  9365  uznfz  10121  elfz0ubfz0  10143  fzoss1  10189  elfzo0z  10202  fzofzim  10206  elfzom1p1elfzo  10232  ssfzo12bi  10243  subfzo0  10260  modfzo0difsn  10413  expaddzap  10582  caucvgre  11008  caubnd2  11144  summodc  11409  fzo0dvdseq  11881  nno  11929  lcmdvds  12097  hashgcdeq  12257  modprm0  12272  pcqcl  12324  issubg4m  13098  01eq0ring  13497  neii1  14044  neii2  14046  fsumcncntop  14453