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  2186  disjiun  4010  euotd  4266  onsucelsucr  4519  isotr  5830  spc2ed  6247  ltbtwnnqq  7427  genpcdl  7531  genpcuu  7532  un0addcl  9222  un0mulcl  9223  btwnnz  9360  uznfz  10116  elfz0ubfz0  10138  fzoss1  10184  elfzo0z  10197  fzofzim  10201  elfzom1p1elfzo  10227  ssfzo12bi  10238  subfzo0  10255  modfzo0difsn  10408  expaddzap  10577  caucvgre  11003  caubnd2  11139  summodc  11404  fzo0dvdseq  11876  nno  11924  lcmdvds  12092  hashgcdeq  12252  modprm0  12267  pcqcl  12319  issubg4m  13082  01eq0ring  13393  neii1  13887  neii2  13889  fsumcncntop  14296