Theorem impancom 258

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 114	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 123	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  eqrdav  2169  disjiun  3982  euotd  4237  onsucelsucr  4490  isotr  5792  spc2ed  6209  ltbtwnnqq  7364  genpcdl  7468  genpcuu  7469  un0addcl  9155  un0mulcl  9156  btwnnz  9293  uznfz  10046  elfz0ubfz0  10068  fzoss1  10114  elfzo0z  10127  fzofzim  10131  elfzom1p1elfzo  10157  ssfzo12bi  10168  subfzo0  10185  modfzo0difsn  10338  expaddzap  10507  caucvgre  10932  caubnd2  11068  summodc  11333  fzo0dvdseq  11804  nno  11852  lcmdvds  12020  hashgcdeq  12180  modprm0  12195  pcqcl  12247  neii1  12900  neii2  12902  fsumcncntop  13309