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

This theorem is referenced by:  mo4  2556  eqrdav  2727  spc2ed  3587  rexraleqim  3632  disjiun  5129  disjord  5130  disjiund  5132  propeqop  5503  euotd  5509  pwssun  5567  iotan0  6532  funopsn  7151  isotr  7338  funeldmb  7361  funfv1st2nd  8044  funelss  8045  el2mpocsbcl  8084  ressuppssdif  8183  oeordi  8601  domunsncan  9090  pssnn  9186  pssnnOLD  9283  findcard3  9303  findcard3OLD  9304  ordtypelem7  9541  inf3lem5  9649  r1tr  9793  cardmin2  10016  ac10ct  10051  isf32lem12  10381  isfin1-3  10403  fin17  10411  fin1a2s  10431  axdc4lem  10472  axcclem  10474  ttukeylem2  10527  genpcd  11023  ltexprlem3  11055  prlem936  11064  supsrlem  11128  mul0or  11878  un0addcl  12529  un0mulcl  12530  btwnnz  12662  uznfz  13610  elfz0ubfz0  13631  elfzo0z  13700  fzofzim  13705  ssfzoulel  13752  ssfzo12bi  13753  subfzo0  13780  modmuladdim  13905  modaddmodup  13925  modfzo0difsn  13934  axdc4uzlem  13974  expaddz  14097  sq01  14213  hashnn0n0nn  14376  hashss  14394  hashgt12el  14407  fi1uzind  14484  brfi1indALT  14487  ccatalpha  14569  swrdswrdlem  14680  swrdswrd  14681  swrdccatin1  14701  pfxccatin12lem3  14708  repswswrd  14760  cshf1  14786  cshw1  14798  2cshwcshw  14802  sqrmo  15224  caubnd2  15330  summo  15689  nno  16352  divalglem8  16370  lcmdvds  16572  lcmfunsnlem1  16601  hashgcdeq  16751  modprm0  16767  pcqcl  16818  vdwnnlem3  16959  prmgaplem5  17017  prmgaplem7  17019  catpropd  17682  cicsym  17780  isinitoi  17981  istermoi  17982  iszeroi  17991  acsfiindd  18538  tsrlemax  18571  issubg4  19093  gsmsymgreqlem2  19379  oddvdsnn0  19492  oddvds  19495  gexdvds  19532  lt6abl  19843  pgpfac1lem3  20027  01eq0ring  20460  isphld  21579  psdmul  22083  coe1ae0  22128  mdetdiaglem  22493  slesolex  22577  pmatcoe1fsupp  22596  cpmatelimp  22607  cpmatelimp2  22609  cpmatmcllem  22613  pm2mpf1  22694  mp2pm2mplem4  22704  fvmptnn04ifa  22745  fvmptnn04ifd  22748  chfacfscmul0  22753  chfacfpmmul0  22757  neii1  23003  neii2  23005  uncmp  23300  isfild  23755  fbunfip  23766  fgss2  23771  fgcl  23775  isufil2  23805  cfinufil  23825  ufilen  23827  fsumcn  24781  lmmbr  25179  iscau4  25200  caussi  25218  cmslssbn  25293  ovoliunnul  25429  ovolicc2lem4  25442  itg1ge0a  25634  rolle  25915  ulmcaulem  26323  cxpge0  26610  fsumvma  27139  gausslemma2dlem1a  27291  2sqb  27358  2sq2  27359  pntrsumbnd2  27493  pntlem3  27535  nofv  27583  sltres  27588  muls0ord  28078  axeuclid  28767  axcontlem2  28769  usgrislfuspgr  28993  nbuhgr2vtx1edgblem  29157  usgredgsscusgredg  29266  upgrwlkvtxedg  29452  uspgr2wlkeq  29453  cyclnspth  29607  uspgrn2crct  29612  crctcshwlkn0lem4  29617  wlkiswwlks2lem5  29677  wlknewwlksn  29691  umgrwwlks2on  29761  clwwlkccatlem  29792  clwlkclwwlklem2a4  29800  clwlkclwwlklem2a  29801  clwwisshclwwslemlem  29816  clwwlkel  29849  wwlksubclwwlk  29861  clwwlknon1  29900  clwwlknonex2lem2  29911  uhgr3cyclexlem  29984  vdgn1frgrv3  30100  2wspmdisj  30140  frgrregord013  30198  spansncvi  31455  lnconi  31836  cdj3lem1  32237  metider  33489  prsrcmpltd  34700  gonar  34999  goalr  35001  satffunlem2lem1  35008  finminlem  35796  clsint2  35807  bj-finsumval0  36758  finxpsuclem  36870  pibt2  36890  wl-exeq  36995  phpreu  37071  poimirlem26  37113  poimir  37120  ismtyima  37270  elpaddn0  39267  tendospcanN  40490  nnproddivdvdsd  41465  dvdsexpnn0  41895  rexzrexnn0  42218  unxpwdom3  42513  unielss  42640  onov0suclim  42697  fsovrfovd  43433  radcnvrat  43745  2reu8i  46487  zm1nn  46676  subsubelfzo0  46700  fzoopth  46701  2ffzoeq  46702  fargshiftf  46774  2pwp1prm  46923  lighneal  46945  isuspgrimlem  47166  isassintop  47266  uzlidlring  47291  2zrngamgm  47301  ply1mulgsumlem1  47448  suppdm  47572  rrxsphere  47815  inlinecirc02plem  47853  pgindnf  48141

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »