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  4088  euotd  4353  onsucelsucr  4612  isotr  5967  spc2ed  6407  nninfninc  7365  ltbtwnnqq  7678  genpcdl  7782  genpcuu  7783  un0addcl  9477  un0mulcl  9478  btwnnz  9618  uznfz  10383  elfz0ubfz0  10405  fzoss1  10453  elfzo0z  10469  fzofzim  10473  elfzom1p1elfzo  10505  ssfzo12bi  10516  subfzo0  10534  modfzo0difsn  10703  expaddzap  10891  ccatalpha  11239  swrdswrdlem  11334  swrdswrd  11335  swrdccatin1  11355  pfxccatin12lem3  11362  caucvgre  11604  caubnd2  11740  summodc  12007  fzo0dvdseq  12481  nno  12530  lcmdvds  12714  hashgcdeq  12875  modprm0  12890  pcqcl  12942  issubg4m  13843  01eq0ring  14267  neii1  14941  neii2  14943  fsumcncntop  15361  gausslemma2dlem1a  15860  usgrislfuspgrdom  16114  upgrwlkvtxedg  16288  uspgr2wlkeq  16289  clwwlkccatlem  16324  clwwlknonex2lem2  16362