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  2228  disjiun  4077  euotd  4340  onsucelsucr  4599  isotr  5939  spc2ed  6377  nninfninc  7286  ltbtwnnqq  7598  genpcdl  7702  genpcuu  7703  un0addcl  9398  un0mulcl  9399  btwnnz  9537  uznfz  10295  elfz0ubfz0  10317  fzoss1  10365  elfzo0z  10380  fzofzim  10384  elfzom1p1elfzo  10415  ssfzo12bi  10426  subfzo0  10443  modfzo0difsn  10612  expaddzap  10800  swrdswrdlem  11231  swrdswrd  11232  swrdccatin1  11252  pfxccatin12lem3  11259  caucvgre  11487  caubnd2  11623  summodc  11889  fzo0dvdseq  12363  nno  12412  lcmdvds  12596  hashgcdeq  12757  modprm0  12772  pcqcl  12824  issubg4m  13725  01eq0ring  14147  neii1  14815  neii2  14817  fsumcncntop  15235  gausslemma2dlem1a  15731  usgrislfuspgrdom  15982