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  2231  disjiun  4104  euotd  4371  onsucelsucr  4630  isotr  5989  spc2ed  6429  nninfninc  7414  ltbtwnnqq  7730  genpcdl  7834  genpcuu  7835  un0addcl  9529  un0mulcl  9530  btwnnz  9672  uznfz  10437  elfz0ubfz0  10459  fzoss1  10507  elfzo0z  10523  fzofzim  10527  elfzom1p1elfzo  10559  ssfzo12bi  10570  subfzo0  10588  modfzo0difsn  10757  expaddzap  10945  ccatalpha  11301  swrdswrdlem  11396  swrdswrd  11397  swrdccatin1  11417  pfxccatin12lem3  11424  caucvgre  11666  caubnd2  11802  summodc  12069  fzo0dvdseq  12543  nno  12592  lcmdvds  12776  hashgcdeq  12937  modprm0  12952  pcqcl  13004  issubg4m  13910  01eq0ring  14334  neii1  15012  neii2  15014  fsumcncntop  15432  gausslemma2dlem1a  15931  usgrislfuspgrdom  16185  upgrwlkvtxedg  16359  uspgr2wlkeq  16360  clwwlkccatlem  16395  clwwlknonex2lem2  16433