Theorem impancom 441

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

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 198  df-an 385

This theorem is referenced by:  eqrdav  2804  rexraleqim  3521  disjiun  4828  disjord  4829  disjiund  4831  propeqop  5159  euotd  5165  pwssun  5212  funopsn  6634  isotr  6807  el2mpt2csbcl  7480  ressuppssdif  7547  oeordi  7901  domunsncan  8296  pssnn  8414  findcard3  8439  ordtypelem7  8665  inf3lem5  8773  r1tr  8883  cardmin2  9104  ac10ct  9137  isf32lem12  9468  isfin1-3  9490  fin17  9498  fin1a2s  9518  axdc4lem  9559  axcclem  9561  ttukeylem2  9614  genpcd  10110  ltexprlem3  10142  prlem936  10151  supsrlem  10214  mul0or  10949  fiminre  11254  un0addcl  11588  un0mulcl  11589  btwnnz  11715  uznfz  12642  elfz0ubfz0  12663  elfzo0z  12730  fzofzim  12735  elfzom1p1elfzo  12768  ssfzoulel  12782  ssfzo12bi  12783  subfzo0  12810  modmuladdim  12933  modaddmodup  12953  modfzo0difsn  12962  axdc4uzlem  13002  expaddz  13123  sq01  13205  hashnn0n0nn  13394  hashss  13410  hashgt12el  13423  fi1uzind  13492  brfi1indALT  13495  ccatalpha  13586  swrdswrdlem  13679  swrdswrd  13680  swrdccatin1  13703  swrdccatin12lem3  13710  repswswrd  13751  cshwmodn  13761  cshf1  13776  cshw1  13788  2cshwcshw  13791  sqrmo  14211  caubnd2  14316  summo  14667  nno  15314  divalglem8  15339  lcmdvds  15536  lcmfunsnlem1  15565  hashgcdeq  15707  modprm0  15723  pcqcl  15774  vdwnnlem3  15914  prmgaplem5  15972  prmgaplem7  15974  catpropd  16569  cicsym  16664  isinitoi  16853  istermoi  16854  iszeroi  16859  acsfiindd  17378  tsrlemax  17421  issubg4  17811  gsmsymgreqlem2  18048  oddvdsnn0  18160  oddvds  18163  gexdvds  18196  lt6abl  18493  pgpfac1lem3  18674  coe1ae0  19790  isphld  20205  mdetdiaglem  20611  slesolex  20696  pmatcoe1fsupp  20715  cpmatelimp  20726  cpmatelimp2  20728  cpmatmcllem  20732  pm2mpf1  20813  mp2pm2mplem4  20823  fvmptnn04ifa  20864  fvmptnn04ifd  20867  chfacfscmul0  20872  chfacfpmmul0  20876  neii1  21120  neii2  21122  uncmp  21416  isfild  21871  fbunfip  21882  fgss2  21887  fgcl  21891  isufil2  21921  cfinufil  21941  ufilen  21943  fsumcn  22882  lmmbr  23264  iscau4  23285  caussi  23303  ovoliunnul  23484  ovolicc2lem4  23497  itg1ge0a  23688  rolle  23963  ulmcaulem  24358  cxpge0  24639  fsumvma  25148  gausslemma2dlem1a  25300  2sqb  25367  pntrsumbnd2  25466  pntlem3  25508  axeuclid  26053  axcontlem2  26055  usgrislfuspgr  26290  nbuhgr2vtx1edgblem  26459  usgredgsscusgredg  26579  upgrwlkvtxedg  26765  uspgr2wlkeq  26766  cyclnspth  26920  uspgrn2crct  26925  crctcshwlkn0lem4  26930  wlkiswwlks2lem5  26996  wlknewwlksn  27010  wlkwwlksurOLD  27021  umgrwwlks2on  27094  clwwlkccatlem  27128  clwwlkccat  27129  clwlkclwwlklem2a4  27136  clwlkclwwlklem2a  27137  clwwisshclwwslemlem  27152  clwwlkel  27191  wwlksubclwwlk  27205  clwlksfoclwwlkOLD  27233  clwwlknon1  27261  clwwlknonex2lem2  27273  uhgr3cyclexlem  27350  vdgn1frgrv3  27468  2wspmdisj  27508  frgrregord013  27579  spansncvi  28836  lnconi  29217  cdj3lem1  29618  spc2ed  29637  metider  30259  funeldmb  31980  nofv  32128  sltres  32133  finminlem  32630  clsint2  32642  bj-finsumval0  33461  finxpsuclem  33547  wl-exeq  33632  phpreu  33703  poimirlem26  33745  poimir  33752  ismtyima  33910  elpaddn0  35577  tendospcanN  36801  rexzrexnn0  37867  unxpwdom3  38163  fsovrfovd  38800  radcnvrat  39010  zm1nn  41889  subsubelfzo0  41908  fzoopth  41909  2ffzoeq  41910  fargshiftf  41948  2pwp1prm  42075  lighneal  42100  isassintop  42411  uzlidlring  42494  2zrngamgm  42504  ply1mulgsumlem1  42739  suppdm  42865