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  2205  disjiun  4046  euotd  4307  onsucelsucr  4564  isotr  5898  spc2ed  6332  nninfninc  7240  ltbtwnnqq  7548  genpcdl  7652  genpcuu  7653  un0addcl  9348  un0mulcl  9349  btwnnz  9487  uznfz  10245  elfz0ubfz0  10267  fzoss1  10315  elfzo0z  10330  fzofzim  10334  elfzom1p1elfzo  10365  ssfzo12bi  10376  subfzo0  10393  modfzo0difsn  10562  expaddzap  10750  swrdswrdlem  11180  swrdswrd  11181  caucvgre  11367  caubnd2  11503  summodc  11769  fzo0dvdseq  12243  nno  12292  lcmdvds  12476  hashgcdeq  12637  modprm0  12652  pcqcl  12704  issubg4m  13604  01eq0ring  14026  neii1  14694  neii2  14696  fsumcncntop  15114  gausslemma2dlem1a  15610