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  2237  disjiun  4120  euotd  4390  onsucelsucr  4650  isotr  6012  spc2ed  6459  nninfninc  7453  ltbtwnnqq  7772  genpcdl  7876  genpcuu  7877  un0addcl  9575  un0mulcl  9576  btwnnz  9719  uznfz  10488  elfz0ubfz0  10510  fzoss1  10558  elfzo0z  10574  fzofzim  10578  elfzom1p1elfzo  10610  ssfzo12bi  10621  subfzo0  10639  modfzo0difsn  10810  expaddzap  10998  ccatalpha  11359  swrdswrdlem  11454  swrdswrd  11455  swrdccatin1  11475  pfxccatin12lem3  11482  caucvgre  11725  caubnd2  11861  summodc  12128  fzo0dvdseq  12602  nno  12651  lcmdvds  12835  hashgcdeq  12996  modprm0  13011  pcqcl  13063  issubg4m  13973  01eq0ring  14469  neii1  15171  neii2  15173  fsumcncntop  15591  gausslemma2dlem1a  16091  usgrislfuspgrdom  16345  upgrwlkvtxedg  16519  uspgr2wlkeq  16520  clwwlkccatlem  16555  clwwlknonex2lem2  16593