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 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  eqrdav  2237  disjiun  4125  euotd  4397  onsucelsucr  4657  isotr  6025  spc2ed  6473  nninfninc  7469  ltbtwnnqq  7788  genpcdl  7892  genpcuu  7893  un0addcl  9607  un0mulcl  9608  btwnnz  9750  uznfz  10526  elfz0ubfz0  10548  fzoss1  10596  elfzo0z  10612  fzofzim  10616  elfzom1p1elfzo  10648  ssfzo12bi  10659  subfzo0  10677  modfzo0difsn  10852  expaddzap  11040  ccatalpha  11402  swrdswrdlem  11497  swrdswrd  11498  swrdccatin1  11518  pfxccatin12lem3  11525  caucvgre  11768  caubnd2  11905  summodc  12174  fzo0dvdseq  12648  nno  12697  lcmdvds  12881  hashgcdeq  13046  modprm0  13061  pcqcl  13113  issubg4m  14054  resscntz  14165  01eq0ring  14604  neii1  15390  neii2  15392  fsumcncntop  15810  gausslemma2dlem1a  16399  usgrislfuspgrdom  16653  upgrwlkvtxedg  16827  uspgr2wlkeq  16828  clwwlkccatlem  16863  clwwlknonex2lem2  16901