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  2203  disjiun  4038  euotd  4297  onsucelsucr  4554  isotr  5875  spc2ed  6309  nninfninc  7207  ltbtwnnqq  7510  genpcdl  7614  genpcuu  7615  un0addcl  9310  un0mulcl  9311  btwnnz  9449  uznfz  10207  elfz0ubfz0  10229  fzoss1  10276  elfzo0z  10289  fzofzim  10293  elfzom1p1elfzo  10324  ssfzo12bi  10335  subfzo0  10352  modfzo0difsn  10521  expaddzap  10709  caucvgre  11211  caubnd2  11347  summodc  11613  fzo0dvdseq  12087  nno  12136  lcmdvds  12320  hashgcdeq  12481  modprm0  12496  pcqcl  12548  issubg4m  13447  01eq0ring  13869  neii1  14537  neii2  14539  fsumcncntop  14957  gausslemma2dlem1a  15453