Theorem impancom 457

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mo4  2596  spc2ed  3562  rexraleqim  3608  prsrcmpltd  4440  disjiun  5099  disjord  5100  disjiund  5102  propeqop  5492  euotd  5498  pwssun  5555  iotan0  6530  funopsn  7148  funopsnOLD  7149  isotr  7340  funeldmb  7365  resf1extb  7933  funfv1st2nd  8045  funelss  8046  el2mpocsbcl  8082  ressuppssdif  8183  oeordi  8575  domunsncan  9068  pssnn  9156  findcard3  9246  ordtypelem7  9489  inf3lem5  9604  r1tr  9751  cardmin2  9997  ac10ct  10030  isf32lem12  10359  isfin1-3  10381  fin17  10389  fin1a2s  10409  axdc4lem  10450  axcclem  10452  ttukeylem2  10505  genpcd  11002  ltexprlem3  11034  prlem936  11043  supsrlem  11107  mul0or  11865  un0addcl  12548  un0mulcl  12549  btwnnz  12683  uznfz  13650  elfz0ubfz0  13672  elfzo0z  13742  fzofzim  13750  ssfzoulel  13801  ssfzo12bi  13802  fzoopth  13803  subfzo0  13834  modmuladdim  13963  modaddmodup  13983  modfzo0difsn  13992  axdc4uzlem  14032  expaddz  14155  sq01  14274  hashnn0n0nn  14440  hashss  14458  hashgt12el  14472  fi1uzind  14557  brfi1indALT  14560  ccatalpha  14645  swrdswrdlem  14758  swrdswrd  14759  swrdccatin1  14779  pfxccatin12lem3  14786  repswswrd  14840  cshf1  14866  cshw1  14878  2cshwcshw  14881  sqrmo  15321  caubnd2  15428  summo  15786  nno  16457  divalglem8  16475  lcmdvds  16683  lcmfunsnlem1  16712  hashgcdeq  16866  modprm0  16882  pcqcl  16933  vdwnnlem3  17074  prmgaplem5  17132  prmgaplem7  17134  catpropd  17782  cicsym  17878  isinitoi  18073  istermoi  18074  iszeroi  18083  acsfiindd  18626  tsrlemax  18659  0gisid  18743  issubg4  19235  gsmsymgreqlem2  19524  oddvdsnn0  19637  oddvds  19640  gexdvds  19677  lt6abl  19988  pgpfac1lem3  20172  01eq0ring  20657  unichnlidl  21391  isphld  21833  psdmul  22358  coe1ae0  22405  mdetdiaglem  22784  slesolex  22868  pmatcoe1fsupp  22887  cpmatelimp  22898  cpmatelimp2  22900  cpmatmcllem  22904  pm2mpf1  22985  mp2pm2mplem4  22995  fvmptnn04ifa  23036  fvmptnn04ifd  23039  chfacfscmul0  23044  chfacfpmmul0  23048  neii1  23292  neii2  23294  uncmp  23589  isfild  24044  fbunfip  24055  fgss2  24060  fgcl  24064  isufil2  24094  cfinufil  24114  ufilen  24116  fsumcn  25058  lmmbr  25446  iscau4  25467  caussi  25485  cmslssbn  25560  ovoliunnul  25695  ovolicc2lem4  25708  itg1ge0a  25899  rolle  26178  ulmcaulem  26586  cxpge0  26877  fsumvma  27406  gausslemma2dlem1a  27558  2sqb  27625  2sq2  27626  pntrsumbnd2  27760  pntlem3  27802  nofv  27850  ltsres  27855  muls0ord  28407  axeuclid  29342  axcontlem2  29344  usgrislfuspgr  29566  nbuhgr2vtx1edgblem  29730  usgredgsscusgredg  29838  upgrwlkvtxedg  30023  uspgr2wlkeq  30024  cyclnspth  30179  uspgrn2crct  30186  crctcshwlkn0lem4  30191  wlkiswwlks2lem5  30251  wlknewwlksn  30265  usgrwwlks2on  30336  umgrwwlks2on  30337  clwwlkccatlem  30369  clwlkclwwlklem2a4  30377  clwlkclwwlklem2a  30378  clwwisshclwwslemlem  30393  clwwlkel  30426  wwlksubclwwlk  30438  clwwlknon1  30477  clwwlknonex2lem2  30488  uhgr3cyclexlem  30561  vdgn1frgrv3  30677  2wspmdisj  30717  frgrregord013  30775  spansncvi  32033  lnconi  32414  cdj3lem1  32815  constrsqrtcl  34192  metider  34307  onvf1odlem4  35606  gonar  35900  goalr  35902  satffunlem2lem1  35909  finminlem  36862  clsint2  36873  cgsex2gd  37814  bj-finsumval0  37962  finxpsuclem  38076  pibt2  38096  wl-exeq  38222  phpreu  38288  poimirlem26  38330  poimir  38337  ismtyima  38487  elpaddn0  40607  tendospcanN  41830  nnproddivdvdsd  42800  dvdsexpnn0  43128  sn-remul0ord  43202  rexzrexnn0  43564  unxpwdom3  43855  unielss  43978  onov0suclim  44034  fsovrfovd  44768  radcnvrat  45057  2reu8i  47883  zm1nn  48072  subsubelfzo0  48097  2ffzoeq  48098  nnmul2  48100  fargshiftf  48222  2pwp1prm  48374  lighneal  48396  isuspgrimlem  48693  upgrimpths  48707  clnbgr3stgrgrlim  48817  gpgedgvtx0  48859  gpgedgvtx1  48860  isassintop  49008  uzlidlring  49033  2zrngamgm  49043  ply1mulgsumlem1  49199  suppdm  49323  rrxsphere  49561  inlinecirc02plem  49599  pgindnf  50527