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  2230  disjiun  4083  euotd  4347  onsucelsucr  4606  isotr  5956  spc2ed  6397  nninfninc  7321  ltbtwnnqq  7634  genpcdl  7738  genpcuu  7739  un0addcl  9434  un0mulcl  9435  btwnnz  9573  uznfz  10337  elfz0ubfz0  10359  fzoss1  10407  elfzo0z  10422  fzofzim  10426  elfzom1p1elfzo  10458  ssfzo12bi  10469  subfzo0  10487  modfzo0difsn  10656  expaddzap  10844  ccatalpha  11189  swrdswrdlem  11284  swrdswrd  11285  swrdccatin1  11305  pfxccatin12lem3  11312  caucvgre  11541  caubnd2  11677  summodc  11943  fzo0dvdseq  12417  nno  12466  lcmdvds  12650  hashgcdeq  12811  modprm0  12826  pcqcl  12878  issubg4m  13779  01eq0ring  14202  neii1  14870  neii2  14872  fsumcncntop  15290  gausslemma2dlem1a  15786  usgrislfuspgrdom  16040  upgrwlkvtxedg  16214  uspgr2wlkeq  16215  clwwlkccatlem  16250  clwwlknonex2lem2  16288