Theorem impancom 451

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mo4  2565  eqrdav  2734  spc2ed  3580  rexraleqim  3626  disjiun  5107  disjord  5108  disjiund  5110  propeqop  5482  euotd  5488  pwssun  5545  iotan0  6520  funopsn  7137  isotr  7328  funeldmb  7351  resf1extb  7928  funfv1st2nd  8043  funelss  8044  el2mpocsbcl  8082  ressuppssdif  8182  oeordi  8597  domunsncan  9084  pssnn  9180  findcard3  9288  findcard3OLD  9289  ordtypelem7  9536  inf3lem5  9644  r1tr  9788  cardmin2  10011  ac10ct  10046  isf32lem12  10376  isfin1-3  10398  fin17  10406  fin1a2s  10426  axdc4lem  10467  axcclem  10469  ttukeylem2  10522  genpcd  11018  ltexprlem3  11050  prlem936  11059  supsrlem  11123  mul0or  11875  un0addcl  12532  un0mulcl  12533  btwnnz  12667  uznfz  13625  elfz0ubfz0  13647  elfzo0z  13716  fzofzim  13724  ssfzoulel  13774  ssfzo12bi  13775  fzoopth  13776  subfzo0  13803  modmuladdim  13930  modaddmodup  13950  modfzo0difsn  13959  axdc4uzlem  13999  expaddz  14122  sq01  14241  hashnn0n0nn  14407  hashss  14425  hashgt12el  14438  fi1uzind  14523  brfi1indALT  14526  ccatalpha  14609  swrdswrdlem  14720  swrdswrd  14721  swrdccatin1  14741  pfxccatin12lem3  14748  repswswrd  14800  cshf1  14826  cshw1  14838  2cshwcshw  14842  sqrmo  15268  caubnd2  15374  summo  15731  nno  16399  divalglem8  16417  lcmdvds  16625  lcmfunsnlem1  16654  hashgcdeq  16807  modprm0  16823  pcqcl  16874  vdwnnlem3  17015  prmgaplem5  17073  prmgaplem7  17075  catpropd  17719  cicsym  17815  isinitoi  18010  istermoi  18011  iszeroi  18020  acsfiindd  18561  tsrlemax  18594  issubg4  19126  gsmsymgreqlem2  19410  oddvdsnn0  19523  oddvds  19526  gexdvds  19563  lt6abl  19874  pgpfac1lem3  20058  01eq0ring  20488  isphld  21612  psdmul  22102  coe1ae0  22150  mdetdiaglem  22534  slesolex  22618  pmatcoe1fsupp  22637  cpmatelimp  22648  cpmatelimp2  22650  cpmatmcllem  22654  pm2mpf1  22735  mp2pm2mplem4  22745  fvmptnn04ifa  22786  fvmptnn04ifd  22789  chfacfscmul0  22794  chfacfpmmul0  22798  neii1  23042  neii2  23044  uncmp  23339  isfild  23794  fbunfip  23805  fgss2  23810  fgcl  23814  isufil2  23844  cfinufil  23864  ufilen  23866  fsumcn  24810  lmmbr  25208  iscau4  25229  caussi  25247  cmslssbn  25322  ovoliunnul  25458  ovolicc2lem4  25471  itg1ge0a  25662  rolle  25944  ulmcaulem  26353  cxpge0  26642  fsumvma  27174  gausslemma2dlem1a  27326  2sqb  27393  2sq2  27394  pntrsumbnd2  27528  pntlem3  27570  nofv  27619  sltres  27624  muls0ord  28128  axeuclid  28888  axcontlem2  28890  usgrislfuspgr  29112  nbuhgr2vtx1edgblem  29276  usgredgsscusgredg  29385  upgrwlkvtxedg  29571  uspgr2wlkeq  29572  cyclnspth  29729  uspgrn2crct  29736  crctcshwlkn0lem4  29741  wlkiswwlks2lem5  29801  wlknewwlksn  29815  umgrwwlks2on  29885  clwwlkccatlem  29916  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwwisshclwwslemlem  29940  clwwlkel  29973  wwlksubclwwlk  29985  clwwlknon1  30024  clwwlknonex2lem2  30035  uhgr3cyclexlem  30108  vdgn1frgrv3  30224  2wspmdisj  30264  frgrregord013  30322  spansncvi  31579  lnconi  31960  cdj3lem1  32361  constrsqrtcl  33759  metider  33871  prsrcmpltd  35058  gonar  35363  goalr  35365  satffunlem2lem1  35372  finminlem  36282  clsint2  36293  bj-finsumval0  37249  finxpsuclem  37361  pibt2  37381  wl-exeq  37498  phpreu  37574  poimirlem26  37616  poimir  37623  ismtyima  37773  elpaddn0  39765  tendospcanN  40988  nnproddivdvdsd  41959  dvdsexpnn0  42330  rexzrexnn0  42774  unxpwdom3  43066  unielss  43189  onov0suclim  43245  fsovrfovd  43980  radcnvrat  44286  2reu8i  47090  zm1nn  47279  subsubelfzo0  47303  2ffzoeq  47304  fargshiftf  47402  2pwp1prm  47551  lighneal  47573  isuspgrimlem  47856  upgrimpths  47870  gpgedgvtx0  48013  gpgedgvtx1  48014  isassintop  48133  uzlidlring  48158  2zrngamgm  48168  ply1mulgsumlem1  48310  suppdm  48434  rrxsphere  48676  inlinecirc02plem  48714  pgindnf  49528