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  2195  disjiun  4029  euotd  4288  onsucelsucr  4545  isotr  5864  spc2ed  6292  nninfninc  7190  ltbtwnnqq  7484  genpcdl  7588  genpcuu  7589  un0addcl  9284  un0mulcl  9285  btwnnz  9422  uznfz  10180  elfz0ubfz0  10202  fzoss1  10249  elfzo0z  10262  fzofzim  10266  elfzom1p1elfzo  10292  ssfzo12bi  10303  subfzo0  10320  modfzo0difsn  10489  expaddzap  10677  caucvgre  11148  caubnd2  11284  summodc  11550  fzo0dvdseq  12024  nno  12073  lcmdvds  12257  hashgcdeq  12418  modprm0  12433  pcqcl  12485  issubg4m  13333  01eq0ring  13755  neii1  14393  neii2  14395  fsumcncntop  14813  gausslemma2dlem1a  15309