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  2203  disjiun  4038  euotd  4298  onsucelsucr  4555  isotr  5884  spc2ed  6318  nninfninc  7224  ltbtwnnqq  7527  genpcdl  7631  genpcuu  7632  un0addcl  9327  un0mulcl  9328  btwnnz  9466  uznfz  10224  elfz0ubfz0  10246  fzoss1  10293  elfzo0z  10306  fzofzim  10310  elfzom1p1elfzo  10341  ssfzo12bi  10352  subfzo0  10369  modfzo0difsn  10538  expaddzap  10726  caucvgre  11234  caubnd2  11370  summodc  11636  fzo0dvdseq  12110  nno  12159  lcmdvds  12343  hashgcdeq  12504  modprm0  12519  pcqcl  12571  issubg4m  13471  01eq0ring  13893  neii1  14561  neii2  14563  fsumcncntop  14981  gausslemma2dlem1a  15477