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  2566  eqrdav  2736  spc2ed  3601  rexraleqim  3647  disjiun  5131  disjord  5132  disjiund  5134  propeqop  5512  euotd  5518  pwssun  5575  iotan0  6551  funopsn  7168  isotr  7356  funeldmb  7379  resf1extb  7956  funfv1st2nd  8071  funelss  8072  el2mpocsbcl  8110  ressuppssdif  8210  oeordi  8625  domunsncan  9112  pssnn  9208  findcard3  9318  findcard3OLD  9319  ordtypelem7  9564  inf3lem5  9672  r1tr  9816  cardmin2  10039  ac10ct  10074  isf32lem12  10404  isfin1-3  10426  fin17  10434  fin1a2s  10454  axdc4lem  10495  axcclem  10497  ttukeylem2  10550  genpcd  11046  ltexprlem3  11078  prlem936  11087  supsrlem  11151  mul0or  11903  un0addcl  12559  un0mulcl  12560  btwnnz  12694  uznfz  13650  elfz0ubfz0  13672  elfzo0z  13741  fzofzim  13749  ssfzoulel  13799  ssfzo12bi  13800  fzoopth  13801  subfzo0  13828  modmuladdim  13955  modaddmodup  13975  modfzo0difsn  13984  axdc4uzlem  14024  expaddz  14147  sq01  14264  hashnn0n0nn  14430  hashss  14448  hashgt12el  14461  fi1uzind  14546  brfi1indALT  14549  ccatalpha  14631  swrdswrdlem  14742  swrdswrd  14743  swrdccatin1  14763  pfxccatin12lem3  14770  repswswrd  14822  cshf1  14848  cshw1  14860  2cshwcshw  14864  sqrmo  15290  caubnd2  15396  summo  15753  nno  16419  divalglem8  16437  lcmdvds  16645  lcmfunsnlem1  16674  hashgcdeq  16827  modprm0  16843  pcqcl  16894  vdwnnlem3  17035  prmgaplem5  17093  prmgaplem7  17095  catpropd  17752  cicsym  17848  isinitoi  18044  istermoi  18045  iszeroi  18054  acsfiindd  18598  tsrlemax  18631  issubg4  19163  gsmsymgreqlem2  19449  oddvdsnn0  19562  oddvds  19565  gexdvds  19602  lt6abl  19913  pgpfac1lem3  20097  01eq0ring  20530  isphld  21672  psdmul  22170  coe1ae0  22218  mdetdiaglem  22604  slesolex  22688  pmatcoe1fsupp  22707  cpmatelimp  22718  cpmatelimp2  22720  cpmatmcllem  22724  pm2mpf1  22805  mp2pm2mplem4  22815  fvmptnn04ifa  22856  fvmptnn04ifd  22859  chfacfscmul0  22864  chfacfpmmul0  22868  neii1  23114  neii2  23116  uncmp  23411  isfild  23866  fbunfip  23877  fgss2  23882  fgcl  23886  isufil2  23916  cfinufil  23936  ufilen  23938  fsumcn  24894  lmmbr  25292  iscau4  25313  caussi  25331  cmslssbn  25406  ovoliunnul  25542  ovolicc2lem4  25555  itg1ge0a  25746  rolle  26028  ulmcaulem  26437  cxpge0  26725  fsumvma  27257  gausslemma2dlem1a  27409  2sqb  27476  2sq2  27477  pntrsumbnd2  27611  pntlem3  27653  nofv  27702  sltres  27707  muls0ord  28211  axeuclid  28978  axcontlem2  28980  usgrislfuspgr  29204  nbuhgr2vtx1edgblem  29368  usgredgsscusgredg  29477  upgrwlkvtxedg  29663  uspgr2wlkeq  29664  cyclnspth  29821  uspgrn2crct  29828  crctcshwlkn0lem4  29833  wlkiswwlks2lem5  29893  wlknewwlksn  29907  umgrwwlks2on  29977  clwwlkccatlem  30008  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwwisshclwwslemlem  30032  clwwlkel  30065  wwlksubclwwlk  30077  clwwlknon1  30116  clwwlknonex2lem2  30127  uhgr3cyclexlem  30200  vdgn1frgrv3  30316  2wspmdisj  30356  frgrregord013  30414  spansncvi  31671  lnconi  32052  cdj3lem1  32453  metider  33893  prsrcmpltd  35095  gonar  35400  goalr  35402  satffunlem2lem1  35409  finminlem  36319  clsint2  36330  bj-finsumval0  37286  finxpsuclem  37398  pibt2  37418  wl-exeq  37535  phpreu  37611  poimirlem26  37653  poimir  37660  ismtyima  37810  elpaddn0  39802  tendospcanN  41025  nnproddivdvdsd  42001  dvdsexpnn0  42369  rexzrexnn0  42815  unxpwdom3  43107  unielss  43230  onov0suclim  43287  fsovrfovd  44022  radcnvrat  44333  2reu8i  47125  zm1nn  47314  subsubelfzo0  47338  2ffzoeq  47339  fargshiftf  47427  2pwp1prm  47576  lighneal  47598  isuspgrimlem  47874  gpgedgvtx0  48019  gpgedgvtx1  48020  isassintop  48126  uzlidlring  48151  2zrngamgm  48161  ply1mulgsumlem1  48303  suppdm  48427  rrxsphere  48669  inlinecirc02plem  48707  pgindnf  49235