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  2233  disjiun  4109  euotd  4376  onsucelsucr  4635  isotr  5995  spc2ed  6442  nninfninc  7427  ltbtwnnqq  7746  genpcdl  7850  genpcuu  7851  un0addcl  9546  un0mulcl  9547  btwnnz  9690  uznfz  10459  elfz0ubfz0  10481  fzoss1  10529  elfzo0z  10545  fzofzim  10549  elfzom1p1elfzo  10581  ssfzo12bi  10592  subfzo0  10610  modfzo0difsn  10781  expaddzap  10969  ccatalpha  11326  swrdswrdlem  11421  swrdswrd  11422  swrdccatin1  11442  pfxccatin12lem3  11449  caucvgre  11691  caubnd2  11827  summodc  12094  fzo0dvdseq  12568  nno  12617  lcmdvds  12801  hashgcdeq  12962  modprm0  12977  pcqcl  13029  issubg4m  13946  01eq0ring  14434  neii1  15138  neii2  15140  fsumcncntop  15558  gausslemma2dlem1a  16057  usgrislfuspgrdom  16311  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  clwwlkccatlem  16521  clwwlknonex2lem2  16559